Let x0 of type ι be given.
Let x1 of type ι be given.
Apply nat_p_omega with
x0.
The subproof is completed by applying H0.
Apply SNoS_E2 with
ordsucc (ordsucc x0),
x1,
SNoLe (eps_ x0) x1 leaving 3 subgoals.
Apply nat_p_ordinal with
ordsucc (ordsucc x0).
Apply nat_ordsucc with
ordsucc x0.
Apply nat_ordsucc with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNoLtLe_or with
x1,
eps_ x0,
SNoLe (eps_ x0) x1 leaving 4 subgoals.
The subproof is completed by applying H6.
Apply SNo_eps_ with
x0.
The subproof is completed by applying L3.
Apply FalseE with
SNoLe (eps_ x0) x1.
Apply SNoLtE with
x1,
eps_ x0,
False leaving 6 subgoals.
The subproof is completed by applying H6.
Apply SNo_eps_ with
x0.
The subproof is completed by applying L3.
The subproof is completed by applying H8.
Let x2 of type ι be given.
Claim L17: x2 = 0
Apply SNoLev_0_eq_0 with
x2 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply eps_ordinal_In_eq_0 with
x0,
SNoLev x2 leaving 2 subgoals.
Apply SNoLev_ordinal with
x2.
The subproof is completed by applying H9.
The subproof is completed by applying H16.
Apply SNoLt_irref with
x1.
Apply SNoLt_tra with
x1,
x2,
x1 leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
The subproof is completed by applying H6.
The subproof is completed by applying H13.
Apply L17 with
λ x3 x4 . SNoLt x4 x1.
The subproof is completed by applying H2.
Claim L12: x1 = 0
Apply SNoLev_0_eq_0 with
x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply eps_ordinal_In_eq_0 with
x0,
SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H11.
Apply SNoLt_irref with
x1.
Apply L12 with
λ x2 x3 . SNoLt x3 x1.
The subproof is completed by applying H2.
Apply SNoLev_eps_ with
x0,
λ x2 x3 . x3 ∈ SNoLev x1 ⟶ SNoEq_ x3 x1 (eps_ x0) ⟶ nIn x3 x1 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L3.
Apply FalseE with
SNoEq_ (ordsucc x0) x1 (eps_ x0) ⟶ nIn (ordsucc x0) x1 ⟶ False.
Apply ordsuccE with
ordsucc x0,
SNoLev x1,
False leaving 3 subgoals.
The subproof is completed by applying H4.
Apply In_no2cycle with
SNoLev x1,
ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H9.
Apply In_irref with
SNoLev x1.
Apply H10 with
λ x2 x3 . x3 ∈ SNoLev x1.
The subproof is completed by applying H9.
The subproof is completed by applying H8.