Let x0 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNoLev x0 ∈ PSNo (ordsucc (SNoLev x0)) (λ x1 . and (x1 ∈ x0) (x1 = SNoLev x0 ⟶ ∀ x2 : ο . x2)).

Apply binunionE with {x1 ∈ ordsucc (SNoLev x0)|(λ x2 . and (x2 ∈ x0) (x2 = SNoLev x0 ⟶ ∀ x3 : ο . x3)) x1}, {(λ x2 . SetAdjoin x2 (Sing 1)) x1|x1 ∈ ordsucc (SNoLev x0),not ((λ x2 . and (x2 ∈ x0) (x2 = SNoLev x0 ⟶ ∀ x3 : ο . x3)) x1)}, SNoLev x0, False leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H2: SNoLev x0 ∈ {x1 ∈ ordsucc (SNoLev x0)|(λ x2 . and (x2 ∈ x0) (x2 = SNoLev x0 ⟶ ∀ x3 : ο . x3)) x1}.

Apply SepE2 with ordsucc (SNoLev x0), λ x1 . and (x1 ∈ x0) (x1 = SNoLev x0 ⟶ ∀ x2 : ο . x2), SNoLev x0, False leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: SNoLev x0 ∈ x0.

Assume H4: SNoLev x0 = SNoLev x0 ⟶ ∀ x1 : ο . x1.

Apply H4.

Let x1 of type ι → ι → ο be given.

Assume H5: x1 (SNoLev x0) (SNoLev x0).

The subproof is completed by applying H5.

Assume H2: SNoLev x0 ∈ {(λ x2 . SetAdjoin x2 (Sing 1)) x1|x1 ∈ ordsucc (SNoLev x0),not ((λ x2 . and (x2 ∈ x0) (x2 = SNoLev x0 ⟶ ∀ x3 : ο . x3)) x1)}.

Apply ReplSepE_impred with ordsucc (SNoLev x0), λ x1 . not ((λ x2 . and (x2 ∈ x0) (x2 = SNoLev x0 ⟶ ∀ x3 : ο . x3)) x1), λ x1 . (λ x2 . SetAdjoin x2 (Sing 1)) x1, SNoLev x0, False leaving 2 subgoals.

The subproof is completed by applying H2.

Let x1 of type ι be given.

Assume H3: x1 ∈ ordsucc (SNoLev x0).

Assume H4: not ((λ x2 . and (x2 ∈ x0) (x2 = SNoLev x0 ⟶ ∀ x3 : ο . x3)) x1).

Assume H5: SNoLev x0 = (λ x2 . SetAdjoin x2 (Sing 1)) x1.

Apply tagged_not_ordinal with x1.

Apply H5 with λ x2 x3 . ordinal x2.

Apply SNoLev_ordinal with x0.

The subproof is completed by applying H0.

■

Proofgold Proof