Apply nat_ind with λ x0 . ∀ x1 . equip x0 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∃ x2 : ι → ι . and (inj x0 x1 x2) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x3 ⟶ x2 x4 ∈ x2 x3) leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: equip 0 x0.

Assume H1: ∀ x1 . x1 ∈ x0 ⟶ ordinal x1.

Let x1 of type ο be given.

Assume H2: ∀ x2 : ι → ι . and (inj 0 x0 x2) (∀ x3 . x3 ∈ 0 ⟶ ∀ x4 . x4 ∈ x3 ⟶ x2 x4 ∈ x2 x3) ⟶ x1.

Apply H2 with λ x2 . x2.

Apply andI with inj 0 x0 (λ x2 . x2), ∀ x2 . x2 ∈ 0 ⟶ ∀ x3 . x3 ∈ x2 ⟶ (λ x4 . x4) x3 ∈ (λ x4 . x4) x2 leaving 2 subgoals.

Apply andI with ∀ x2 . x2 ∈ 0 ⟶ (λ x3 . x3) x2 ∈ x0, ∀ x2 . x2 ∈ 0 ⟶ ∀ x3 . x3 ∈ 0 ⟶ (λ x4 . x4) x2 = (λ x4 . x4) x3 ⟶ x2 = x3 leaving 2 subgoals.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with (λ x3 . x3) x2 ∈ x0.

Apply EmptyE with x2.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with ∀ x3 . x3 ∈ 0 ⟶ (λ x4 . x4) x2 = (λ x4 . x4) x3 ⟶ x2 = x3.

Apply EmptyE with x2.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with ∀ x3 . x3 ∈ x2 ⟶ (λ x4 . x4) x3 ∈ (λ x4 . x4) x2.

Apply EmptyE with x2.

The subproof is completed by applying H3.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . equip x0 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∃ x2 : ι → ι . and (inj x0 x1 x2) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x3 ⟶ x2 x4 ∈ x2 x3).

Let x1 of type ι be given.

Assume H2: equip (ordsucc x0) x1.

Assume H3: ∀ x2 . x2 ∈ x1 ⟶ ordinal x2.

Apply H2 with ∃ x2 : ι → ι . and (inj (ordsucc x0) x1 x2) (∀ x3 . x3 ∈ ordsucc x0 ⟶ ∀ x4 . x4 ∈ x3 ⟶ x2 x4 ∈ x2 x3).

Let x2 of type ι → ι be given.

Assume H4: bij (ordsucc x0) x1 x2.

Apply H4 with ∃ x3 : ι → ι . and (inj (ordsucc x0) x1 x3) (∀ x4 . x4 ∈ ordsucc x0 ⟶ ∀ x5 . x5 ∈ x4 ⟶ x3 x5 ∈ x3 x4).

Assume H5: and (∀ x3 . x3 ∈ ordsucc x0 ⟶ x2 x3 ∈ x1) (∀ x3 . ... ⟶ ∀ x4 . ... ⟶ x2 x3 = ... ⟶ x3 = x4).

...

■

Proofgold Proof