| pf |
|---|
Apply set_ext with SNoL 1, 1 leaving 2 subgoals.
Let x0 of type ι be given.
Apply SNoL_E with 1, x0, x0 ∈ 1 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying H0.
Apply ordinal_SNoLev with 1, λ x1 x2 . SNoLev x0 ∈ x2 ⟶ SNoLt x0 1 ⟶ x0 ∈ 1 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
Claim L4: 0 = x0
Apply SNo_eq with 0, x0 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H1.
Apply SNoLev_0 with λ x1 x2 . x2 = SNoLev x0.
Apply cases_1 with SNoLev x0, λ x1 . 0 = x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x1 of type ι → ι → ο be given.
Assume H4: x1 0 0.
The subproof is completed by applying H4.
Apply SNoLev_0 with λ x1 x2 . SNoEq_ x2 0 x0.
Apply SNoEq_I with 0, 0, x0.
Let x1 of type ι be given.
Assume H4: x1 ∈ 0.
Apply FalseE with iff (x1 ∈ 0) (x1 ∈ x0).
Apply EmptyE with x1.
The subproof is completed by applying H4.
Apply L4 with λ x1 x2 . x1 ∈ 1.
The subproof is completed by applying In_0_1.
Let x0 of type ι be given.
Assume H0: x0 ∈ 1.
Apply cases_1 with x0, λ x1 . x1 ∈ SNoL 1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoL_I with 1, 0 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with λ x1 x2 . x2 ∈ SNoLev 1.
Apply ordinal_SNoLev with 1, λ x1 x2 . 0 ∈ x2 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
The subproof is completed by applying In_0_1.
Apply ordinal_In_SNoLt with 1, 0 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
The subproof is completed by applying In_0_1.
■ |
|