Let x0 of type ι be given.
Apply nat_ind with
λ x1 . ∃ x2 . and (x2 ⊆ x0) (equip x2 x1) leaving 2 subgoals.
Let x1 of type ο be given.
Assume H1:
∀ x2 . and (x2 ⊆ x0) (equip x2 0) ⟶ x1.
Apply H1 with
0.
Apply andI with
0 ⊆ x0,
equip 0 0 leaving 2 subgoals.
The subproof is completed by applying Subq_Empty with x0.
The subproof is completed by applying equip_ref with 0.
Let x1 of type ι be given.
Assume H2:
∃ x2 . and (x2 ⊆ x0) (equip x2 x1).
Apply H2 with
∃ x2 . and (x2 ⊆ x0) (equip x2 (ordsucc x1)).
Let x2 of type ι be given.
Assume H3:
(λ x3 . and (x3 ⊆ x0) (equip x3 x1)) x2.
Apply H3 with
∃ x3 . and (x3 ⊆ x0) (equip x3 (ordsucc x1)).
Assume H4: x2 ⊆ x0.
Apply H5 with
∃ x3 . and (x3 ⊆ x0) (equip x3 (ordsucc x1)).
Let x3 of type ι → ι be given.
Apply H6 with
∃ x4 . and (x4 ⊆ x0) (equip x4 (ordsucc x1)).
Assume H7:
and (∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x1) (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5).
Apply H7 with
(∀ x4 . x4 ∈ x1 ⟶ ∃ x5 . and (x5 ∈ x2) (x3 x5 = x4)) ⟶ ∃ x4 . and (x4 ⊆ x0) (equip x4 (ordsucc x1)).
Assume H8: ∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x1.
Assume H9: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Assume H10:
∀ x4 . x4 ∈ x1 ⟶ ∃ x5 . and (x5 ∈ x2) (x3 x5 = x4).
Apply dneg with
∃ x4 . and (x4 ∈ x0) (nIn x4 x2),
∃ x4 . and (x4 ⊆ x0) (equip x4 (ordsucc x1)) leaving 2 subgoals.
Assume H11:
not (∃ x4 . and (x4 ∈ x0) (nIn x4 x2)).
Apply H0.
Let x4 of type ο be given.
Apply H12 with
x1.
Apply andI with
x1 ∈ omega,
equip x0 x1 leaving 2 subgoals.
Apply nat_p_omega with
x1.
The subproof is completed by applying H1.
Apply set_ext with
x2,
x0,
λ x5 x6 . equip x5 x1 leaving 3 subgoals.
The subproof is completed by applying H4.
Let x5 of type ι be given.
Assume H13: x5 ∈ x0.
Apply dneg with
x5 ∈ x2.
Apply H11.
Let x6 of type ο be given.
Assume H15:
∀ x7 . and (x7 ∈ x0) (nIn x7 x2) ⟶ x6.
Apply H15 with
x5.
Apply andI with
x5 ∈ x0,
nIn x5 x2 leaving 2 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H5.