Let x be given.
Assume Hx.
Let alpha be given.
Assume Ha.
We prove the intermediate claim Lx1: SNo_ (SNoLev x) x.
An exact proof term for the current goal is SNoLev_ x Hx.
Apply Lx1 to the current goal.
Assume Hx1: x ⊆ SNoElts_ (SNoLev x).
Assume Hx2: ∀beta ∈ SNoLev x, exactly1of2 (SetAdjoin beta {1} ∈ x) (beta ∈ x).
We will prove x ∩ SNoElts_ alpha ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (SetAdjoin beta {1} ∈ x ∩ SNoElts_ alpha) (beta ∈ x ∩ SNoElts_ alpha).
Apply andI to the current goal.
An exact proof term for the current goal is binintersect_Subq_2 x (SNoElts_ alpha).
Let beta be given.
Assume Hb: beta ∈ alpha.
We prove the intermediate claim Lb: beta ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) alpha Ha beta Hb.
Apply exactly1of2_E (SetAdjoin beta {1} ∈ x) (beta ∈ x) (Hx2 beta Lb) to the current goal.
Assume H1: SetAdjoin beta {1} ∈ x.
Assume H2: beta ∉ x.
Apply exactly1of2_I1 to the current goal.
Apply binintersectI to the current goal.
An exact proof term for the current goal is H1.
We will prove SetAdjoin beta {1} ∈ SNoElts_ alpha.
We will prove SetAdjoin beta {1} ∈ alpha ∪ {SetAdjoin beta {1}|beta ∈ alpha}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is ReplI alpha (λbeta ⇒ SetAdjoin beta {1}) beta Hb.
We will prove beta ∉ x ∩ SNoElts_ alpha.
Assume H3.
An exact proof term for the current goal is H2 (binintersectE1 x (SNoElts_ alpha) beta H3).
Assume H1: SetAdjoin beta {1} ∉ x.
Assume H2: beta ∈ x.
Apply exactly1of2_I2 to the current goal.
Assume H3: SetAdjoin beta {1} ∈ x ∩ SNoElts_ alpha.
An exact proof term for the current goal is H1 (binintersectE1 x (SNoElts_ alpha) (SetAdjoin beta {1}) H3).
Apply binintersectI to the current goal.
An exact proof term for the current goal is H2.
We will prove beta ∈ SNoElts_ alpha.
We will prove beta ∈ alpha ∪ {SetAdjoin beta {1}|beta ∈ alpha}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hb.
∎