Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CSNo x0.
Apply CSNo_E with x0, λ x1 . ExtendedSNoElt_ 3 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: x0 = SNo_pair x1 x2.
Let x3 of type ι be given.
Assume H4: x3 ∈ prim3 (SNo_pair x1 x2).
Apply UnionE_impred with SNo_pair x1 x2, x3, or (ordinal x3) (∃ x4 . and (x4 ∈ 3) (x3 = Sing x4)) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x4 of type ι be given.
Assume H5: x3 ∈ x4.
Assume H6: x4 ∈ SNo_pair x1 x2.
Apply binunionE with x1, {(λ x6 . SetAdjoin x6 (Sing 2)) x5|x5 ∈ x2}, x4, or (ordinal x3) (∃ x5 . and (x5 ∈ 3) (x3 = Sing x5)) leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H7: x4 ∈ x1.
Claim L8: x3 ∈ prim3 x1
Apply UnionI with x1, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Apply extension_SNoElt_mon with 2, 3, x1, x3 leaving 3 subgoals.
The subproof is completed by applying ordsuccI1 with 2.
Apply SNo_ExtendedSNoElt_2 with x1.
The subproof is completed by applying H1.
The subproof is completed by applying L8.
Assume H7: x4 ∈ {(λ x6 . SetAdjoin x6 (Sing 2)) x5|x5 ∈ x2}.
Apply ReplE_impred with x2, λ x5 . SetAdjoin x5 (Sing 2), x4, or (ordinal x3) (∃ x5 . and (x5 ∈ 3) (x3 = Sing x5)) leaving 2 subgoals.
The subproof is completed by applying H7.
Let x5 of type ι be given.
Assume H8: x5 ∈ x2.
Assume H9: x4 = (λ x6 . SetAdjoin x6 (Sing 2)) x5.
Claim L10: x3 ∈ (λ x6 . SetAdjoin x6 (Sing 2)) x5
Apply H9 with λ x6 x7 . x3 ∈ x6.
The subproof is completed by applying H5.
Apply binunionE with x5, Sing (Sing 2), x3, or (ordinal x3) (∃ x6 . and (x6 ∈ 3) (x3 = Sing x6)) leaving 3 subgoals.
The subproof is completed by applying L10.
Assume H11: x3 ∈ x5.
Claim L12: x3 ∈ prim3 x2
Apply UnionI with x2, x3, x5 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H8.
Apply extension_SNoElt_mon with 2, 3, x2, x3 leaving 3 subgoals.
The subproof is completed by applying ordsuccI1 with 2.
Apply SNo_ExtendedSNoElt_2 with x2.
The subproof is completed by applying H2.
The subproof is completed by applying L12.
Assume H11: x3 ∈ Sing (Sing 2).
Apply orIR with ordinal x3, ∃ x6 . and (x6 ∈ 3) (x3 = Sing x6).
Let x6 of type ο be given.
Assume H12: ∀ x7 . and (x7 ∈ 3) (x3 = Sing x7) ⟶ x6.
Apply H12 with 2.
Apply andI with 2 ∈ 3, x3 = Sing 2 leaving 2 subgoals.
The subproof is completed by applying In_2_3.
Apply SingE with Sing 2, x3.
The subproof is completed by applying H11.
■