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: (λ x3 . SetAdjoin x3 (Sing x0)) x2 ∈ x1.
Apply SNoLev_prop with x1, False leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H4: ordinal (SNoLev x1).
Assume H5: SNo_ (SNoLev x1) x1.
Apply H5 with False.
Assume H6: x1 ⊆ SNoElts_ (SNoLev x1).
Apply FalseE with (∀ x3 . x3 ∈ SNoLev x1 ⟶ exactly1of2 (SetAdjoin x3 (Sing 1) ∈ x1) (x3 ∈ x1)) ⟶ False.
Claim L7: (λ x3 . SetAdjoin x3 (Sing x0)) x2 ∈ binunion (SNoLev x1) {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ SNoLev x1}
Apply H6 with (λ x3 . SetAdjoin x3 (Sing x0)) x2.
The subproof is completed by applying H3.
Apply binunionE with SNoLev x1, {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ SNoLev x1}, (λ x3 . SetAdjoin x3 (Sing x0)) x2, False leaving 3 subgoals.
The subproof is completed by applying L7.
Assume H8: (λ x3 . SetAdjoin x3 (Sing x0)) x2 ∈ SNoLev x1.
Apply unknownprop_ffc171453ac798e185a4c4fc0de7bb85ce44d8ec72157829e9ddfc0f80032171 with x0, SNoLev x1, x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Assume H8: (λ x3 . SetAdjoin x3 (Sing x0)) x2 ∈ {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ SNoLev x1}.
Apply ReplE_impred with SNoLev x1, λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3, (λ x3 . SetAdjoin x3 (Sing x0)) x2, False leaving 2 subgoals.
The subproof is completed by applying H8.
Let x3 of type ι be given.
Assume H9: x3 ∈ SNoLev x1.
Assume H10: (λ x4 . SetAdjoin x4 (Sing x0)) x2 = (λ x4 . SetAdjoin x4 (Sing 1)) x3.
Claim L11: ordinal x3
Apply ordinal_Hered with SNoLev x1, x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
Claim L12: Sing x0 ∈ (λ x4 . SetAdjoin x4 (Sing 1)) x3
Apply H10 with λ x4 x5 . Sing x0 ∈ x4.
Apply binunionI2 with x2, Sing (Sing x0), Sing x0.
The subproof is completed by applying SingI with Sing x0.
Apply binunionE with x3, Sing (Sing 1), Sing x0, False leaving 3 subgoals.
The subproof is completed by applying L12.
Assume H13: Sing x0 ∈ x3.
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 L11.
The subproof is completed by applying H13.
Apply unknownprop_e948d7c5fa1375f6d519e47d896028dd041b0af5587408f5c508216bbae8d46d with x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■