Let alpha be given.

Assume Ha: ordinal alpha.

Let x be given.

Let beta be given.

Assume Hb: beta ∈ alpha.

Assume H1: SNo_ beta x.

Apply H1 to the current goal.

Assume H2: x ⊆ SNoElts_ beta.

Assume H3: ∀gamma ∈ beta, exactly1of2 (gamma ' ∈ x) (gamma ∈ x).

We will prove x ∈ SNoS_ alpha.

We will prove x ∈ {x ∈ 𝒫 (SNoElts_ alpha)|∃gamma ∈ alpha, SNo_ gamma x}.

Apply SepI to the current goal.

We will prove x ∈ 𝒫 (SNoElts_ alpha).

Apply PowerI to the current goal.

We will prove x ⊆ SNoElts_ alpha.

Apply Subq_tra x (SNoElts_ beta) (SNoElts_ alpha) H2 to the current goal.

We will prove SNoElts_ beta ⊆ SNoElts_ alpha.

Apply SNoElts_mon to the current goal.

Apply Ha to the current goal.

Assume Ha1 _.

An exact proof term for the current goal is Ha1 beta Hb.

We will prove ∃gamma ∈ alpha, SNo_ gamma x.

We use beta to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is H1.

∎