Apply Empty_Subq_eq with SNoL 0.

Let x0 of type ι be given.

Assume H0: x0 ∈ SNoL 0.

Claim L1: x0 ∈ SNoS_ 0

Apply SNoLev_0 with λ x1 x2 . x0 ∈ SNoS_ x1.

Apply SNoL_SNoS_ with 0, x0.

The subproof is completed by applying H0.

Apply SNoS_E2 with 0, x0, x0 ∈ 0 leaving 3 subgoals.

The subproof is completed by applying ordinal_Empty.

The subproof is completed by applying L1.

Assume H2: SNoLev x0 ∈ 0.

Apply FalseE with ordinal (SNoLev x0) ⟶ SNo x0 ⟶ SNo_ (SNoLev x0) x0 ⟶ x0 ∈ 0.

Apply EmptyE with SNoLev x0.

The subproof is completed by applying H2.

■

Proofgold Proof