Let x0 of type ι → ο be given.
Assume H0:
∀ x1 x2 . SNoCutP x1 x2 ⟶ (∀ x3 . x3 ∈ x1 ⟶ x0 x3) ⟶ (∀ x3 . x3 ∈ x2 ⟶ x0 x3) ⟶ x0 (SNoCut x1 x2).
Claim L1:
∀ x1 . ordinal x1 ⟶ ∀ x2 . SNo x2 ⟶ SNoLev x2 ∈ x1 ⟶ x0 x2
Apply ordinal_ind with
λ x1 . ∀ x2 . SNo x2 ⟶ SNoLev x2 ∈ x1 ⟶ x0 x2.
Let x1 of type ι be given.
Assume H2:
∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . SNo x3 ⟶ SNoLev x3 ∈ x2 ⟶ x0 x3.
Let x2 of type ι be given.
Apply SNoLev_ordinal with
x2.
The subproof is completed by applying H3.
Apply SNo_etaE with
x2,
x0 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H7:
∀ x5 . x5 ∈ x3 ⟶ SNoLev x5 ∈ SNoLev x2.
Assume H8:
∀ x5 . x5 ∈ x4 ⟶ SNoLev x5 ∈ SNoLev x2.
Apply H6 with
x0 x2.
Assume H10:
and (∀ x5 . x5 ∈ x3 ⟶ SNo x5) (∀ x5 . x5 ∈ x4 ⟶ SNo x5).
Apply H10 with
(∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x4 ⟶ SNoLt x5 x6) ⟶ x0 x2.
Assume H11:
∀ x5 . x5 ∈ x3 ⟶ SNo x5.
Assume H12:
∀ x5 . x5 ∈ x4 ⟶ SNo x5.
Assume H13:
∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x4 ⟶ SNoLt x5 x6.
Apply H9 with
λ x5 x6 . x0 x6.
Apply H0 with
x3,
x4 leaving 3 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H14: x5 ∈ x3.
Apply H2 with
SNoLev x2,
x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H11 with
x5.
The subproof is completed by applying H14.
Apply H7 with
x5.
The subproof is completed by applying H14.
Let x5 of type ι be given.
Assume H14: x5 ∈ x4.
Apply H2 with
SNoLev x2,
x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H12 with
x5.
The subproof is completed by applying H14.
Apply H8 with
x5.
The subproof is completed by applying H14.
Let x1 of type ι be given.
Apply ordinal_ordsucc with
SNoLev x1.
Apply SNoLev_ordinal with
x1.
The subproof is completed by applying H2.
Apply L1 with
ordsucc (SNoLev x1),
x1 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H2.
The subproof is completed by applying ordsuccI2 with
SNoLev x1.