| pf |
|---|
Apply nat_ind with λ x0 . equip {x1 ∈ SNoS_ omega|SNoLev x1 = x0} (exp_SNo_nat 2 x0) leaving 2 subgoals.
Apply exp_SNo_nat_0 with 2, λ x0 x1 . equip {x2 ∈ SNoS_ omega|SNoLev x2 = 0} x1 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply equip_sym with 1, {x0 ∈ SNoS_ omega|SNoLev x0 = 0}.
Let x0 of type ο be given.
Apply H0 with λ x1 . 0.
Apply bijI with 1, {x1 ∈ SNoS_ omega|SNoLev x1 = 0}, λ x1 . 0 leaving 3 subgoals.
Let x1 of type ι be given.
Assume H1: x1 ∈ 1.
Apply SepI with SNoS_ omega, λ x2 . SNoLev x2 = 0, 0 leaving 2 subgoals.
Apply SNoS_I with omega, 0, 0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
Apply ordinal_SNo_ with 0.
The subproof is completed by applying ordinal_Empty.
The subproof is completed by applying SNoLev_0.
Let x1 of type ι be given.
Assume H1: x1 ∈ 1.
Let x2 of type ι be given.
Assume H2: x2 ∈ 1.
Assume H3: 0 = 0.
Apply cases_1 with x1, λ x3 . x3 = x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply cases_1 with x2, λ x3 . 0 = x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply SepE with SNoS_ omega, λ x2 . SNoLev x2 = 0, x1, ∃ x2 . and (x2 ∈ 1) ((λ x3 . 0) x2 = x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply SNoS_E2 with omega, x1, ∃ x2 . and (x2 ∈ 1) ((λ x3 . 0) x2 = x1) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H2.
Let x2 of type ο be given.
Assume H8: ∀ x3 . and (x3 ∈ 1) ((λ x4 . 0) x3 = x1) ⟶ x2. Apply H8 with 0.
Apply andI with 0 ∈ 1, (λ x3 . 0) 0 = x1 leaving 2 subgoals.
The subproof is completed by applying In_0_1.
Let x3 of type ι → ι → ο be given.
Apply SNo_eq with 0, x1, λ x4 x5 . (λ x6 x7 . x3 x7 x6) x5 x4 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H6.
Apply SNoLev_0 with λ x4 x5 . x5 = SNoLev x1.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H3 with λ x5 x6 . x4 x6 x5.
Apply SNoLev_0 with λ x4 x5 . SNoEq_ x5 0 x1.
Let x4 of type ι be given.
Assume H9: x4 ∈ 0.
Apply FalseE with iff (x4 ∈ 0) (x4 ∈ x1).
Apply EmptyE with x4.
The subproof is completed by applying H9.
Let x0 of type ι be given.
Apply exp_SNo_nat_S with 2, x0, λ x1 x2 . equip {x3 ∈ SNoS_ omega|SNoLev x3 = ordsucc x0} x2 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
■ |
|