Let α be given.
Assume Ha: ordinal α.
Let z be given.
Assume Hz: SNo z.
Assume Hz2: SNoLev z ∈ α.
We prove the intermediate claim La1: SNo α.
An exact proof term for the current goal is ordinal_SNo α Ha.
We prove the intermediate claim La2: SNoLev α = α.
An exact proof term for the current goal is ordinal_SNoLev α Ha.
We will prove z < α.
Apply SNoLt_trichotomy_or z α Hz (ordinal_SNo α Ha) to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: z < α.
An exact proof term for the current goal is H1.
Assume H1: z = α.
We will prove False.
Apply In_irref α to the current goal.
rewrite the current goal using La2 (from right to left) at position 1.
We will prove SNoLev α ∈ α.
rewrite the current goal using H1 (from right to left) at position 1.
We will prove SNoLev z ∈ α.
An exact proof term for the current goal is Hz2.
Assume H1: α < z.
We will prove False.
Apply SNoLtE α z La1 Hz H1 to the current goal.
Let w be given.
rewrite the current goal using La2 (from left to right).
Assume Hw: SNo w.
Assume H2: SNoLev w ∈ α ∩ SNoLev z.
Assume H3: SNoEq_ (SNoLev w) w α.
Assume H4: SNoEq_ (SNoLev w) w z.
Assume H5: α < w.
Assume H6: w < z.
Assume H7: SNoLev w ∉ α.
We will prove False.
Apply H7 to the current goal.
An exact proof term for the current goal is binintersectE1 α (SNoLev z) (SNoLev w) H2.
rewrite the current goal using La2 (from left to right).
Assume H2: α ∈ SNoLev z.
We will prove False.
An exact proof term for the current goal is In_no2cycle α (SNoLev z) H2 Hz2.
rewrite the current goal using La2 (from left to right).
Assume H2: SNoLev z ∈ α.
Assume H3: SNoEq_ (SNoLev z) α z.
Assume H4: SNoLev z ∉ α.
An exact proof term for the current goal is H4 H2.
∎