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 ∈ SNoS_ (ordsucc x0).
Assume H2: SNoLt 0 x1.
Assume H3: SNoEq_ (SNoLev x1) (eps_ x0) x1.
Apply SNoS_E2 with ordsucc x0, x1, ∃ x2 . and (x2 ∈ x0) (x1 = eps_ x2) leaving 3 subgoals.
Apply nat_p_ordinal with ordsucc x0.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H4: SNoLev x1 ∈ ordsucc x0.
Assume H5: ordinal (SNoLev x1).
Assume H6: SNo x1.
Assume H7: SNo_ (SNoLev x1) x1.
Claim L8: nat_p ...
...
Apply nat_inv with SNoLev x1, ∃ x2 . and (x2 ∈ x0) (x1 = eps_ x2) leaving 3 subgoals.
The subproof is completed by applying L8.
Assume H9: SNoLev x1 = 0.
Apply FalseE with ∃ x2 . and (x2 ∈ x0) (x1 = eps_ x2).
Claim L10: x1 = 0
Apply SNoLev_0_eq_0 with x1 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
Apply SNoLt_irref with x1.
Apply L10 with λ x2 x3 . SNoLt x3 x1.
The subproof is completed by applying H2.
Assume H9: ∃ x2 . and (nat_p x2) (SNoLev x1 = ordsucc x2).
Apply H9 with ∃ x2 . and (x2 ∈ x0) (x1 = eps_ x2).
Let x2 of type ι be given.
Assume H10: (λ x3 . and (nat_p x3) (SNoLev x1 = ordsucc x3)) x2.
Apply H10 with ∃ x3 . and (x3 ∈ x0) (x1 = eps_ x3).
Assume H11: nat_p x2.
Assume H12: SNoLev x1 = ordsucc x2.
Let x3 of type ο be given.
Assume H13: ∀ x4 . and (x4 ∈ x0) (x1 = eps_ x4) ⟶ x3.
Apply H13 with x2.
Apply andI with x2 ∈ x0, x1 = eps_ x2 leaving 2 subgoals.
Apply nat_ordsucc_trans with x0, SNoLev x1, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply H12 with λ x4 x5 . x2 ∈ x5.
The subproof is completed by applying ordsuccI2 with x2.
Apply SNo_eq with x1, eps_ x2 leaving 4 subgoals.
The subproof is completed by applying H6.
Apply SNo_eps_ with x2.
Apply nat_p_omega with x2.
The subproof is completed by applying H11.
Apply SNoLev_eps_ with x2, λ x4 x5 . SNoLev x1 = x5 leaving 2 subgoals.
Apply nat_p_omega with x2.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Apply SNoEq_tra_ with SNoLev x1, x1, eps_ x0, eps_ x2 leaving 2 subgoals.
Apply SNoEq_sym_ with SNoLev x1, eps_ x0, x1.
The subproof is completed by applying H3.
Apply H12 with λ x4 x5 . SNoEq_ x5 (eps_ x0) (eps_ x2).
Apply SNoEq_I with ordsucc x2, eps_ x0, eps_ x2.
Let x4 of type ι be given.
Assume H14: x4 ∈ ordsucc x2.
Claim L15: ordinal x4
Apply nat_p_ordinal with x4.
Apply nat_p_trans with ordsucc x2, x4 leaving 2 subgoals.
Apply nat_ordsucc with x2.
The subproof is completed by applying H11.
The subproof is completed by applying H14.
Apply iffI with x4 ∈ eps_ x0, x4 ∈ eps_ x2 leaving 2 subgoals.
Assume H16: x4 ∈ eps_ x0.
Apply eps_ordinal_In_eq_0 with x0, x4, λ x5 x6 . x6 ∈ eps_ x2 leaving 3 subgoals.
The subproof is completed by applying L15.
The subproof is completed by applying H16.
Apply binunionI1 with Sing 0, {SetAdjoin (ordsucc x5) (Sing 1)|x5 ∈ x2}, 0.
The subproof is completed by applying SingI with 0.
Assume H16: x4 ∈ eps_ x2.
Apply eps_ordinal_In_eq_0 with x2, x4, λ x5 x6 . x6 ∈ eps_ x0 leaving 3 subgoals.
The subproof is completed by applying L15.
The subproof is completed by applying H16.
Apply binunionI1 with Sing 0, {SetAdjoin (ordsucc x5) (Sing 1)|x5 ∈ x0}, 0.
The subproof is completed by applying SingI with 0.
■