Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: HSNo x0.
Apply HSNo_E with x0, λ x1 . ExtendedSNoElt_ 4 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: CSNo x1.
Assume H2: CSNo x2.
Assume H3: x0 = CSNo_pair x1 x2.
Let x3 of type ι be given.
Assume H4: x3 ∈ prim3 (CSNo_pair x1 x2).
Apply UnionE_impred with CSNo_pair x1 x2, x3, or (ordinal x3) (∃ x4 . and (x4 ∈ 4) (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 ∈ CSNo_pair x1 x2.
Apply binunionE with x1, {(λ x6 . SetAdjoin x6 (Sing 3)) x5|x5 ∈ x2}, x4, or (ordinal x3) (∃ x5 . and (x5 ∈ 4) (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 3, 4, x1, x3 leaving 3 subgoals.
The subproof is completed by applying ordsuccI1 with 3.
Apply CSNo_ExtendedSNoElt_3 with x1.
The subproof is completed by applying H1.
The subproof is completed by applying L8.
Assume H7: x4 ∈ {(λ x6 . SetAdjoin x6 (Sing 3)) x5|x5 ∈ x2}.
Apply ReplE_impred with x2, λ x5 . SetAdjoin x5 (Sing 3), x4, or (ordinal x3) (∃ x5 . and (x5 ∈ 4) (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 3)) x5.
Claim L10: x3 ∈ (λ x6 . SetAdjoin x6 (Sing 3)) x5
Apply H9 with λ x6 x7 . x3 ∈ x6.
The subproof is completed by applying H5.
Apply binunionE with x5, Sing (Sing 3), x3, or (ordinal x3) (∃ x6 . and (x6 ∈ 4) (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 3, 4, x2, x3 leaving 3 subgoals.
The subproof is completed by applying ordsuccI1 with 3.
Apply CSNo_ExtendedSNoElt_3 with x2.
The subproof is completed by applying H2.
The subproof is completed by applying L12.
Assume H11: x3 ∈ Sing (Sing 3).
Apply orIR with ordinal x3, ∃ x6 . and (x6 ∈ 4) (x3 = Sing x6).
Let x6 of type ο be given.
Assume H12: ∀ x7 . and (x7 ∈ 4) (x3 = Sing x7) ⟶ x6.
Apply H12 with 3.
Apply andI with 3 ∈ 4, x3 = Sing 3 leaving 2 subgoals.
The subproof is completed by applying In_3_4.
Apply SingE with Sing 3, x3.
The subproof is completed by applying H11.
■