Let x0 of type ι be given.
Apply SNoLtE with
0,
x0,
x0 = 1 leaving 6 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply FalseE with
SNoEq_ (SNoLev x1) x1 0 ⟶ SNoEq_ (SNoLev x1) x1 x0 ⟶ SNoLt 0 x1 ⟶ SNoLt x1 x0 ⟶ nIn (SNoLev x1) 0 ⟶ SNoLev x1 ∈ x0 ⟶ x0 = 1.
Apply EmptyE with
SNoLev x1.
Apply ordinal_SNoLev with
0,
λ x2 x3 . SNoLev x1 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply binintersectE1 with
SNoLev 0,
SNoLev x0,
SNoLev x1.
The subproof is completed by applying H4.
Apply ordinal_SNoLev with
0,
λ x1 x2 . x2 ∈ SNoLev x0 ⟶ SNoEq_ x2 0 x0 ⟶ x2 ∈ x0 ⟶ x0 = 1 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
Assume H5: 0 ∈ x0.
Apply set_ext with
SNoLev x0,
1 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H6: x1 ∈ 1.
Apply cases_1 with
x1,
λ x2 . x2 ∈ SNoLev x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H3.
Apply SNo_eq with
x0,
1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply ordinal_SNoLev with
1,
λ x1 x2 . SNoLev x0 = x2 leaving 2 subgoals.
Apply nat_p_ordinal with
1.
The subproof is completed by applying nat_1.
The subproof is completed by applying L6.
Apply L6 with
λ x1 x2 . SNoEq_ x2 x0 1.
Let x1 of type ι be given.
Assume H7: x1 ∈ 1.
Apply cases_1 with
x1,
λ x2 . iff (x2 ∈ x0) (x2 ∈ 1) leaving 2 subgoals.
The subproof is completed by applying H7.
Apply iffI with
0 ∈ x0,
0 ∈ 1 leaving 2 subgoals.
Assume H8: 0 ∈ x0.
The subproof is completed by applying In_0_1.
Assume H8: 0 ∈ 1.
The subproof is completed by applying H5.
Apply FalseE with
SNoEq_ (SNoLev x0) 0 x0 ⟶ nIn (SNoLev x0) 0 ⟶ x0 = 1.
Apply EmptyE with
SNoLev x0.
Apply ordinal_SNoLev with
0,
λ x1 x2 . SNoLev x0 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
The subproof is completed by applying H3.