Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Assume H1: (λ x2 . SetAdjoin x2 (Sing 2)) x1 ∈ x0.

Apply H0 with False.

Let x2 of type ι be given.

Assume H2: (λ x3 . and (ordinal x3) (SNo_ x3 x0)) x2.

Apply H2 with False.

Assume H3: ordinal x2.

Assume H4: SNo_ x2 x0.

Apply H4 with False.

Assume H5: x0 ⊆ SNoElts_ x2.

Apply FalseE with (∀ x3 . x3 ∈ x2 ⟶ exactly1of2 (SetAdjoin x3 (Sing 1) ∈ x0) (x3 ∈ x0)) ⟶ False.

Claim L6: (λ x3 . SetAdjoin x3 (Sing 2)) x1 ∈ binunion x2 {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x2}

Apply H5 with (λ x3 . SetAdjoin x3 (Sing 2)) x1.

The subproof is completed by applying H1.

Apply binunionE with x2, {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x2}, (λ x3 . SetAdjoin x3 (Sing 2)) x1, False leaving 3 subgoals.

The subproof is completed by applying L6.

Assume H7: (λ x3 . SetAdjoin x3 (Sing 2)) x1 ∈ x2.

Apply ctagged_notin_ordinal with x2, x1 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H7.

Assume H7: (λ x3 . SetAdjoin x3 (Sing 2)) x1 ∈ {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x2}.

Apply ReplE_impred with x2, λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3, (λ x3 . SetAdjoin x3 (Sing 2)) x1, False leaving 2 subgoals.

The subproof is completed by applying H7.

Let x3 of type ι be given.

Assume H8: x3 ∈ x2.

Assume H9: (λ x4 . SetAdjoin x4 (Sing 2)) x1 = (λ x4 . SetAdjoin x4 (Sing 1)) x3.

Claim L10: ordinal x3

Apply ordinal_Hered with x2, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H8.

Claim L11: Sing 2 ∈ (λ x4 . SetAdjoin x4 (Sing 1)) x3

Apply H9 with λ x4 x5 . Sing 2 ∈ x4.

Apply binunionI2 with x1, Sing (Sing 2), Sing 2.

The subproof is completed by applying SingI with Sing 2.

Apply binunionE with x3, Sing (Sing 1), Sing 2, False leaving 3 subgoals.

The subproof is completed by applying L11.

Assume H12: Sing 2 ∈ x3.

Apply unknownprop_7bb148020ac74fad9e588d8f6f24c2245db7c295ea73aac9a7af2c90be710bd6.

Apply ordinal_Hered with x3, Sing 2 leaving 2 subgoals.

The subproof is completed by applying L10.

The subproof is completed by applying H12.

The subproof is completed by applying Sing2_notin_SingSing1.

■

Proofgold Proof