Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ ordsucc x0.
Claim L2: ...
...
Let x2 of type ο be given.
Assume H3: ∀ x3 : ι → ι . bij x0 (setminus (ordsucc x0) (Sing x1)) x3 ⟶ x2.
Apply H3 with λ x3 . If_i (x3 ∈ x1) x3 (ordsucc x3).
Apply bijI with x0, setminus (ordsucc x0) (Sing x1), λ x3 . If_i (x3 ∈ x1) x3 (ordsucc x3) leaving 3 subgoals.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Apply xm with x3 ∈ x1, (λ x4 . If_i (x4 ∈ x1) x4 (ordsucc x4)) x3 ∈ setminus (ordsucc x0) (Sing x1) leaving 2 subgoals.
Assume H5: x3 ∈ x1.
Apply If_i_1 with x3 ∈ x1, x3, ordsucc x3, λ x4 x5 . x5 ∈ setminus (ordsucc x0) (Sing x1) leaving 2 subgoals.
The subproof is completed by applying H5.
Apply setminusI with ordsucc x0, Sing x1, x3 leaving 2 subgoals.
Apply ordsuccI1 with x0, x3.
The subproof is completed by applying H4.
Assume H6: x3 ∈ Sing x1.
Apply In_irref with x3.
Apply SingE with x1, x3, λ x4 x5 . x3 ∈ x5 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Assume H5: nIn x3 x1.
Apply If_i_0 with x3 ∈ x1, x3, ordsucc x3, λ x4 x5 . x5 ∈ setminus (ordsucc x0) (Sing x1) leaving 2 subgoals.
The subproof is completed by applying H5.
Apply setminusI with ordsucc x0, Sing x1, ordsucc x3 leaving 2 subgoals.
Apply nat_ordsucc_in_ordsucc with x0, x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H6: ordsucc x3 ∈ Sing x1.
Apply H5.
Apply SingE with x1, ordsucc x3, λ x4 x5 . x3 ∈ x4 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying ordsuccI2 with x3.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Let x4 of type ι be given.
Assume H5: x4 ∈ x0.
Apply xm with x3 ∈ x1, (λ x5 . If_i (x5 ∈ x1) x5 (ordsucc x5)) x3 = (λ x5 . If_i (x5 ∈ x1) x5 (ordsucc x5)) x4 ⟶ x3 = x4 leaving 2 subgoals.
Assume H6: x3 ∈ x1.
Apply If_i_1 with x3 ∈ x1, x3, ordsucc x3, λ x5 x6 . x6 = (λ x7 . If_i (x7 ∈ x1) x7 (ordsucc x7)) x4 ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply xm with x4 ∈ x1, x3 = (λ x5 . If_i (x5 ∈ x1) x5 (ordsucc x5)) x4 ⟶ x3 = x4 leaving 2 subgoals.
Assume H7: x4 ∈ x1.
Apply If_i_1 with x4 ∈ x1, x4, ordsucc x4, λ x5 x6 . x3 = x6 ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H8: x3 = x4.
The subproof is completed by applying H8.
Assume H7: nIn x4 x1.
Apply If_i_0 with x4 ∈ x1, x4, ordsucc x4, λ x5 x6 . x3 = x6 ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H8: x3 = ordsucc x4.
Apply FalseE with x3 = x4.
Claim L9: ordsucc x4 ∈ x1
Apply H8 with λ x5 x6 . x5 ∈ x1.
The subproof is completed by applying H6.
Apply H7.
Apply nat_trans with x1, ordsucc x4, x4 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L9.
The subproof is completed by applying ordsuccI2 with x4.
Assume H6: nIn x3 x1.
...
...
■