Let x be given.
Assume Hx.
Let α 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: ∀β ∈ SNoLev x, exactly1of2 (SetAdjoin β {1} ∈ x) (β ∈ x).
We will prove x ∩ SNoElts_ α ⊆ SNoElts_ α ∧ ∀β ∈ α, exactly1of2 (SetAdjoin β {1} ∈ x ∩ SNoElts_ α) (β ∈ x ∩ SNoElts_ α).
Apply andI to the current goal.
An exact proof term for the current goal is binintersect_Subq_2 x (SNoElts_ α).
Let β be given.
Assume Hb: β ∈ α.
We prove the intermediate claim Lb: β ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) α Ha β Hb.
Apply exactly1of2_E (SetAdjoin β {1} ∈ x) (β ∈ x) (Hx2 β Lb) to the current goal.
Assume H1: SetAdjoin β {1} ∈ x.
Assume H2: β ∉ 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 β {1} ∈ SNoElts_ α.
We will prove SetAdjoin β {1} ∈ α ∪ {SetAdjoin β {1}|β ∈ α}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is ReplI α (λβ ⇒ SetAdjoin β {1}) β Hb.
We will prove β ∉ x ∩ SNoElts_ α.
Assume H3.
An exact proof term for the current goal is H2 (binintersectE1 x (SNoElts_ α) β H3).
Assume H1: SetAdjoin β {1} ∉ x.
Assume H2: β ∈ x.
Apply exactly1of2_I2 to the current goal.
Assume H3: SetAdjoin β {1} ∈ x ∩ SNoElts_ α.
An exact proof term for the current goal is H1 (binintersectE1 x (SNoElts_ α) (SetAdjoin β {1}) H3).
Apply binintersectI to the current goal.
An exact proof term for the current goal is H2.
We will prove β ∈ SNoElts_ α.
We will prove β ∈ α ∪ {SetAdjoin β {1}|β ∈ α}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hb.
∎