Let α be given.
Assume Ha: ordinal α.
Let x be given.
Let β be given.
Assume Hb: β ∈ α.
Assume H1: SNo_ β x.
Apply H1 to the current goal.
Assume H2: x ⊆ SNoElts_ β.
Assume H3: ∀γ ∈ β, exactly1of2 (γ ' ∈ x) (γ ∈ x).
We will prove x ∈ SNoS_ α.
We will prove x ∈ {x ∈ 𝒫 (SNoElts_ α)|∃γ ∈ α, SNo_ γ x}.
Apply SepI to the current goal.
We will prove x ∈ 𝒫 (SNoElts_ α).
Apply PowerI to the current goal.
We will prove x ⊆ SNoElts_ α.
Apply Subq_tra x (SNoElts_ β) (SNoElts_ α) H2 to the current goal.
We will prove SNoElts_ β ⊆ SNoElts_ α.
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 β Hb.
We will prove ∃γ ∈ α, SNo_ γ x.
We use β 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.
∎