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.
Assume H2: x0 = x1 ⟶ ∀ x2 : ο . x2.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H3: SNo x3.
Assume H4: x4 ∈ x3.
Assume H5: (λ x5 . SetAdjoin x5 (Sing x0)) x2 = (λ x5 . SetAdjoin x5 (Sing x1)) x4.
Claim L6: Sing x0 ∈ (λ x5 . SetAdjoin x5 (Sing x1)) x4
Apply H5 with λ x5 x6 . Sing x0 ∈ x5.
Apply binunionI2 with x2, Sing (Sing x0), Sing x0.
The subproof is completed by applying SingI with Sing x0.
Apply binunionE with x4, Sing (Sing x1), Sing x0, False leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7: Sing x0 ∈ x4.
Apply SNoLev_ with x3, False leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H8: x3 ⊆ SNoElts_ (SNoLev x3).
Assume H9: ∀ x5 . x5 ∈ SNoLev x3 ⟶ exactly1of2 (SetAdjoin x5 (Sing 1) ∈ x3) (x5 ∈ x3).
Apply binunionE with SNoLev x3, {(λ x6 . SetAdjoin x6 (Sing 1)) x5|x5 ∈ SNoLev x3}, x4, False leaving 3 subgoals.
Apply H8 with x4.
The subproof is completed by applying H4.
Assume H10: x4 ∈ SNoLev x3.
Claim L11: ordinal x4
Apply ordinal_Hered with SNoLev x3, x4 leaving 2 subgoals.
Apply SNoLev_ordinal with x3.
The subproof is completed by applying H3.
The subproof is completed by applying H10.
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 x4, Sing x0 leaving 2 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying H7.
Assume H10: x4 ∈ {(λ x6 . SetAdjoin x6 (Sing 1)) x5|x5 ∈ SNoLev x3}.
Apply ReplE_impred with SNoLev x3, λ x5 . SetAdjoin x5 (Sing 1), x4, False leaving 2 subgoals.
The subproof is completed by applying H10.
Let x5 of type ι be given.
Assume H11: x5 ∈ SNoLev x3.
Assume H12: x4 = (λ x6 . SetAdjoin x6 (Sing 1)) x5.
Claim L13: Sing x0 ∈ binunion x5 (Sing (Sing 1))
Apply H12 with λ x6 x7 . Sing x0 ∈ x6.
The subproof is completed by applying H7.
Claim L14: ordinal x5
Apply ordinal_Hered with SNoLev x3, x5 leaving 2 subgoals.
Apply SNoLev_ordinal with x3.
The subproof is completed by applying H3.
The subproof is completed by applying H11.
Apply binunionE with x5, Sing (Sing 1), Sing x0, False leaving 3 subgoals.
The subproof is completed by applying L13.
Assume H15: Sing x0 ∈ x5.
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 x5, Sing x0 leaving 2 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying H15.
Assume H15: Sing x0 ∈ Sing (Sing 1).
Claim L16: Sing x0 = Sing 1
Apply SingE with Sing 1, Sing x0.
The subproof is completed by applying H15.
Apply In_irref with 1.
Apply Sing_inj with x0, 1, λ x6 x7 . 1 ∈ x6 leaving 2 subgoals.
The subproof is completed by applying L16.
The subproof is completed by applying H1.
Assume H7: Sing x0 ∈ Sing (Sing x1).
Apply H2.
Apply Sing_inj with x0, x1.
Apply SingE with Sing x1, Sing x0.
The subproof is completed by applying H7.
■