Let x0 of type ι be given.

Assume H0: SNo x0.

Let x1 of type ι be given.

Assume H1: x1 ∈ prim3 x0.

Apply UnionE_impred with x0, x1, or (ordinal x1) (∃ x2 . and (x2 ∈ 2) (x1 = Sing x2)) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: x1 ∈ x2.

Assume H3: x2 ∈ x0.

Apply SNoLev_ with x0, or (ordinal x1) (∃ x3 . and (x3 ∈ 2) (x1 = Sing x3)) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H4: x0 ⊆ SNoElts_ (SNoLev x0).

Assume H5: ∀ x3 . x3 ∈ SNoLev x0 ⟶ exactly1of2 (SetAdjoin x3 (Sing 1) ∈ x0) (x3 ∈ x0).

Apply binunionE with SNoLev x0, {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ SNoLev x0}, x2, or (ordinal x1) (∃ x3 . and (x3 ∈ 2) (x1 = Sing x3)) leaving 3 subgoals.

Apply H4 with x2.

The subproof is completed by applying H3.

Assume H6: x2 ∈ SNoLev x0.

Claim L7: ordinal x2

Apply ordinal_Hered with SNoLev x0, x2 leaving 2 subgoals.

Apply SNoLev_ordinal with x0.

The subproof is completed by applying H0.

The subproof is completed by applying H6.

Apply orIL with ordinal x1, ∃ x3 . and (x3 ∈ 2) (x1 = Sing x3).

Apply ordinal_Hered with x2, x1 leaving 2 subgoals.

The subproof is completed by applying L7.

The subproof is completed by applying H2.

Assume H6: x2 ∈ {(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ SNoLev x0}.

Apply ReplE_impred with SNoLev x0, λ x3 . SetAdjoin x3 (Sing 1), x2, or (ordinal x1) (∃ x3 . and (x3 ∈ 2) (x1 = Sing x3)) leaving 2 subgoals.

The subproof is completed by applying H6.

Let x3 of type ι be given.

Assume H7: x3 ∈ SNoLev x0.

Assume H8: x2 = (λ x4 . SetAdjoin x4 (Sing 1)) x3.

Claim L9: x1 ∈ (λ x4 . SetAdjoin x4 (Sing 1)) x3

Apply H8 with λ x4 x5 . x1 ∈ x4.

The subproof is completed by applying H2.

Apply binunionE with x3, Sing (Sing 1), x1, or (ordinal x1) (∃ x4 . and (x4 ∈ 2) (x1 = Sing x4)) leaving 3 subgoals.

The subproof is completed by applying L9.

Assume H10: x1 ∈ x3.

Claim L11: ordinal x3

Apply ordinal_Hered with SNoLev x0, x3 leaving 2 subgoals.

Apply SNoLev_ordinal with x0.

The subproof is completed by applying H0.

The subproof is completed by applying H7.

Apply orIL with ordinal x1, ∃ x4 . and (x4 ∈ 2) (x1 = Sing x4).

Apply ordinal_Hered with x3, x1 leaving 2 subgoals.

The subproof is completed by applying L11.

The subproof is completed by applying H10.

Assume H10: x1 ∈ Sing (Sing 1).

Apply orIR with ordinal x1, ∃ x4 . and (x4 ∈ 2) (x1 = Sing x4).

Let x4 of type ο be given.

Assume H11: ∀ x5 . and (x5 ∈ 2) (x1 = Sing x5) ⟶ x4.

Apply H11 with 1.

Apply andI with 1 ∈ 2, x1 = Sing 1 leaving 2 subgoals.

The subproof is completed by applying In_1_2.

Apply SingE with Sing 1, x1.

The subproof is completed by applying H10.

■

Proofgold Proof