Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Let x1 of type ι be given.
Assume H1: x1 ∈ x0.
Claim L2: nat_p x0
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Claim L3: nat_p x1
Apply nat_p_trans with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H1.
Claim L4: x1 ∈ omega
Apply nat_p_omega with x1.
The subproof is completed by applying L3.
Apply SNoLtI3 with eps_ x0, eps_ x1 leaving 3 subgoals.
Apply SNoLev_eps_ with x1, λ x2 x3 . x3 ∈ SNoLev (eps_ x0) leaving 2 subgoals.
The subproof is completed by applying L4.
Apply SNoLev_eps_ with x0, λ x2 x3 . ordsucc x1 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply nat_ordsucc_in_ordsucc with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H1.
Apply SNoLev_eps_ with x1, λ x2 x3 . SNoEq_ x3 (eps_ x0) (eps_ x1) leaving 2 subgoals.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Assume H5: x2 ∈ ordsucc x1.
Claim L6: ordinal x2
Apply nat_p_ordinal with x2.
Apply nat_p_trans with ordsucc x1, x2 leaving 2 subgoals.
Apply nat_ordsucc with x1.
The subproof is completed by applying L3.
The subproof is completed by applying H5.
Apply iffI with x2 ∈ eps_ x0, x2 ∈ eps_ x1 leaving 2 subgoals.
Assume H7: x2 ∈ eps_ x0.
Apply eps_ordinal_In_eq_0 with x0, x2, λ x3 x4 . x4 ∈ eps_ x1 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Apply binunionI1 with Sing 0, {(λ x4 . SetAdjoin x4 (Sing 1)) (ordsucc x3)|x3 ∈ x1}, 0.
The subproof is completed by applying SingI with 0.
Assume H7: x2 ∈ eps_ x1.
Apply eps_ordinal_In_eq_0 with x1, x2, λ x3 x4 . x4 ∈ eps_ x0 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Apply binunionI1 with Sing 0, {(λ x4 . SetAdjoin x4 (Sing 1)) (ordsucc x3)|x3 ∈ x0}, 0.
The subproof is completed by applying SingI with 0.
Apply SNoLev_eps_ with x1, λ x2 x3 . nIn x3 (eps_ x0) leaving 2 subgoals.
The subproof is completed by applying L4.
Assume H5: ordsucc x1 ∈ eps_ x0.
Apply neq_ordsucc_0 with x1.
Apply eps_ordinal_In_eq_0 with x0, ordsucc x1 leaving 2 subgoals.
Apply ordinal_ordsucc with x1.
Apply nat_p_ordinal with x1.
The subproof is completed by applying L3.
The subproof is completed by applying H5.
■