Let x0 of type ι be given.
Assume H0:
∀ x1 . x1 ∈ x0 ⟶ SNo x1.
Apply H1 with
(x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ ∃ x1 . SNo_max_of x0 x1.
Let x1 of type ι be given.
Apply H2 with
(x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ ∃ x2 . SNo_max_of x0 x2.
Apply nat_inv with
x1,
equip x0 x1 ⟶ (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ ∃ x2 . SNo_max_of x0 x2 leaving 3 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H3.
Assume H4: x1 = 0.
Apply H4 with
λ x2 x3 . equip x0 x3 ⟶ (x0 = 0 ⟶ ∀ x4 : ο . x4) ⟶ ∃ x4 . SNo_max_of x0 x4.
Assume H6: x0 = 0 ⟶ ∀ x2 : ο . x2.
Apply FalseE with
∃ x2 . SNo_max_of x0 x2.
Apply H5 with
False.
Let x2 of type ι → ι be given.
Apply bijE with
x0,
0,
x2,
False leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H8: ∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ 0.
Assume H9: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H10:
∀ x3 . x3 ∈ 0 ⟶ ∃ x4 . and (x4 ∈ x0) (x2 x4 = x3).
Apply H6.
Apply Empty_eq with
x0.
Let x3 of type ι be given.
Assume H11: x3 ∈ x0.
Apply EmptyE with
x2 x3.
Apply H8 with
x3.
The subproof is completed by applying H11.
Apply H4 with
equip x0 x1 ⟶ (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ ∃ x2 . SNo_max_of x0 x2.
Let x2 of type ι be given.
Apply H5 with
equip x0 x1 ⟶ (x0 = 0 ⟶ ∀ x3 : ο . x3) ⟶ ∃ x3 . SNo_max_of x0 x3.
Apply H7 with
λ x3 x4 . equip x0 x4 ⟶ (x0 = 0 ⟶ ∀ x5 : ο . x5) ⟶ ∃ x5 . SNo_max_of x0 x5.
Assume H9: x0 = 0 ⟶ ∀ x3 : ο . x3.
Apply nat_ind with
λ x3 . ∀ x4 . (∀ x5 . x5 ∈ x4 ⟶ SNo x5) ⟶ equip x4 (ordsucc x3) ⟶ ∃ x5 . SNo_max_of x4 x5,
x2,
x0 leaving 5 subgoals.
Let x3 of type ι be given.
Assume H10:
∀ x4 . x4 ∈ x3 ⟶ SNo x4.
Apply equip_sym with
x3,
1,
∃ x4 . SNo_max_of x3 x4 leaving 2 subgoals.
The subproof is completed by applying H11.
Let x4 of type ι → ι be given.
Apply bijE with
1,
x3,
x4,
∃ x5 . SNo_max_of x3 x5 leaving 2 subgoals.
The subproof is completed by applying H12.
Assume H13: ∀ x5 . ... ⟶ ... ∈ ....