Let x0 of type ι be given.
Apply SNoS_E2 with
ordsucc omega,
x0,
∃ x1 . and (x1 ∈ omega) (SNoLt x0 x1) leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H0.
Apply SNoLtE with
x0,
omega,
∃ x1 . and (x1 ∈ omega) (SNoLt x0 x1) leaving 6 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply H14 with
SNoLev x1.
Apply andI with
SNoLev x1 ∈ omega,
SNoLt x0 (SNoLev x1) leaving 2 subgoals.
The subproof is completed by applying H13.
Apply SNoLtLe_tra with
x0,
x1,
SNoLev x1 leaving 5 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Apply ordinal_SNo with
SNoLev x1.
Apply SNoLev_ordinal with
x1.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply ordinal_SNoLev_max_2 with
SNoLev x1,
x1 leaving 3 subgoals.
Apply SNoLev_ordinal with
x1.
The subproof is completed by applying H6.
The subproof is completed by applying H6.
The subproof is completed by applying ordsuccI2 with
SNoLev x1.
Let x1 of type ο be given.
Apply H9 with
ordsucc (SNoLev x0).
Apply andI with
ordsucc (SNoLev x0) ∈ omega,
SNoLt x0 (ordsucc (SNoLev x0)) leaving 2 subgoals.
Apply omega_ordsucc with
SNoLev x0.
The subproof is completed by applying H8.
Apply ordinal_SNoLev_max with
ordsucc (SNoLev x0),
x0 leaving 3 subgoals.
Apply ordinal_ordsucc with
SNoLev x0.
Apply SNoLev_ordinal with
x0.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
The subproof is completed by applying ordsuccI2 with
SNoLev x0.
Apply ordinal_SNoLev with
omega,
λ x1 x2 . x2 ∈ SNoLev x0 ⟶ SNoEq_ x2 x0 omega ⟶ nIn x2 x0 ⟶ ∃ x3 . and (x3 ∈ omega) (SNoLt x0 x3) leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
Apply FalseE with
SNoEq_ omega x0 omega ⟶ nIn omega x0 ⟶ ∃ x1 . and (x1 ∈ omega) (SNoLt x0 x1).
Apply ordsuccE with
omega,
SNoLev x0,
False leaving 3 subgoals.
The subproof is completed by applying H2.
Apply In_no2cycle with
SNoLev x0,
omega leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
Apply In_irref with
omega.
Apply H7 with
λ x1 x2 . omega ∈ x1.
The subproof is completed by applying H6.