Apply nat_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ ∀ x2 . infinite x2 ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ⊆ x2 ⟶ equip x4 x1 ⟶ x3 x4 ∈ x0) ⟶ ∃ x4 . and (x4 ⊆ x2) (∃ x5 . and (x5 ∈ x0) (and (infinite x4) (∀ x6 . x6 ⊆ x4 ⟶ equip x6 x1 ⟶ x3 x6 = x5))) leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι be given.

Assume H1: infinite x1.

Let x2 of type ι → ι be given.

Assume H2: ∀ x3 . x3 ⊆ x1 ⟶ equip x3 x0 ⟶ x2 x3 ∈ 0.

Apply FalseE with ∃ x3 . and (x3 ⊆ x1) (∃ x4 . and (x4 ∈ 0) (and (infinite x3) (∀ x5 . x5 ⊆ x3 ⟶ equip x5 x0 ⟶ x2 x5 = x4))).

Apply infinite_Finite_Subq_ex with x1, x0, False leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H0.

Let x3 of type ι be given.

Assume H3: (λ x4 . and (x4 ⊆ x1) (equip x4 x0)) x3.

Apply H3 with False.

Assume H4: x3 ⊆ x1.

Assume H5: equip x3 x0.

Apply EmptyE with x2 x3.

Apply H2 with x3 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . nat_p x1 ⟶ ∀ x2 . infinite x2 ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ⊆ x2 ⟶ equip x4 x1 ⟶ x3 x4 ∈ x0) ⟶ ∃ x4 . and (x4 ⊆ x2) (∃ x5 . and (x5 ∈ x0) (and (infinite x4) (∀ x6 . x6 ⊆ x4 ⟶ equip x6 x1 ⟶ x3 x6 = x5))).

Apply nat_ind with λ x1 . ∀ x2 . infinite x2 ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ⊆ x2 ⟶ equip x4 x1 ⟶ x3 x4 ∈ ordsucc x0) ⟶ ∃ x4 . and (x4 ⊆ x2) (∃ x5 . and (x5 ∈ ordsucc x0) (and (infinite x4) (∀ x6 . x6 ⊆ x4 ⟶ equip x6 x1 ⟶ x3 x6 = x5))) leaving 2 subgoals.

Let x1 of type ι be given.

Assume H2: infinite x1.

Let x2 of type ι → ι be given.

Assume H3: ∀ x3 . x3 ⊆ x1 ⟶ equip x3 0 ⟶ x2 x3 ∈ ordsucc x0.

Let x3 of type ο be given.

Assume H4: ∀ x4 . and (x4 ⊆ x1) (∃ x5 . and (x5 ∈ ordsucc x0) (and (infinite x4) (∀ x6 . x6 ⊆ x4 ⟶ equip x6 0 ⟶ x2 x6 = x5))) ⟶ x3.

Apply H4 with x1.

Apply andI with x1 ⊆ x1, ∃ x4 . and (x4 ∈ ordsucc x0) (and (infinite x1) (∀ x5 . x5 ⊆ x1 ⟶ equip x5 0 ⟶ x2 x5 = x4)) leaving 2 subgoals.

...

■

Proofgold Proof