Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: 1 ∈ x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H2: SNo x1.
Assume H3: SNo x2.
Let x3 of type ι be given.
Assume H4: x3 ∈ x1.
Let x4 of type ι be given.
Assume H5: x4 ∈ x2.
Assume H6: (λ x5 . SetAdjoin x5 (Sing x0)) x3 = (λ x5 . SetAdjoin x5 (Sing x0)) x4.
Let x5 of type ι be given.
Assume H7: x5 ∈ x3.
Claim L8: x5 ∈ (λ x6 . SetAdjoin x6 (Sing x0)) x4
Apply H6 with λ x6 x7 . x5 ∈ x6.
Apply binunionI1 with x3, Sing (Sing x0), x5.
The subproof is completed by applying H7.
Apply binunionE with x4, Sing (Sing x0), x5, x5 ∈ x4 leaving 3 subgoals.
The subproof is completed by applying L8.
Assume H9: x5 ∈ x4.
The subproof is completed by applying H9.
Assume H9: x5 ∈ Sing (Sing x0).
Apply FalseE with x5 ∈ x4.
Claim L10: x5 = Sing x0
Apply SingE with Sing x0, x5.
The subproof is completed by applying H9.
Claim L11: Sing x0 ∈ x3
Apply L10 with λ x6 x7 . x6 ∈ x3.
The subproof is completed by applying H7.
Apply SNoLev_prop with x1, False leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H12: ordinal (SNoLev x1).
Assume H13: SNo_ (SNoLev x1) x1.
Apply H13 with False.
Assume H14: x1 ⊆ SNoElts_ (SNoLev x1).
Apply FalseE with (∀ x6 . x6 ∈ SNoLev x1 ⟶ exactly1of2 (SetAdjoin x6 (Sing 1) ∈ x1) (x6 ∈ x1)) ⟶ False.
Apply binunionE with SNoLev x1, {(λ x7 . SetAdjoin x7 (Sing 1)) x6|x6 ∈ SNoLev x1}, x3, False leaving 3 subgoals.
Apply H14 with x3.
The subproof is completed by applying H4.
Assume H15: x3 ∈ SNoLev x1.
Claim L16: ordinal x3
Apply ordinal_Hered with SNoLev x1, x3 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H15.
Apply not_ordinal_Sing_tagn with x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply ordinal_Hered with x3, Sing x0 leaving 2 subgoals.
The subproof is completed by applying L16.
The subproof is completed by applying L11.
Assume H15: x3 ∈ {(λ x7 . SetAdjoin x7 (Sing 1)) x6|x6 ∈ SNoLev x1}.
Apply ReplE_impred with SNoLev x1, λ x6 . (λ x7 . SetAdjoin x7 (Sing 1)) x6, x3, False leaving 2 subgoals.
The subproof is completed by applying H15.
Let x6 of type ι be given.
Assume H16: x6 ∈ SNoLev x1.
Assume H17: x3 = (λ x7 . SetAdjoin x7 (Sing 1)) x6.
Claim L18: ordinal x6
Apply ordinal_Hered with SNoLev x1, x6 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H16.
Claim L19: Sing x0 ∈ (λ x7 . SetAdjoin x7 (Sing 1)) x6
Apply H17 with λ x7 x8 . Sing x0 ∈ x7.
The subproof is completed by applying L11.
Apply binunionE with x6, Sing (Sing 1), Sing x0, False leaving 3 subgoals.
The subproof is completed by applying L19.
Assume H20: Sing x0 ∈ x6.
Apply not_ordinal_Sing_tagn with x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply ordinal_Hered with x6, Sing x0 leaving 2 subgoals.
The subproof is completed by applying L18.
The subproof is completed by applying H20.
Apply unknownprop_e948d7c5fa1375f6d519e47d896028dd041b0af5587408f5c508216bbae8d46d with x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■