Apply nat_ind with λ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ ordsucc x0 ⟶ x1 x2 ∈ x0) ⟶ not (∀ x2 . x2 ∈ ordsucc x0 ⟶ ∀ x3 . x3 ∈ ordsucc x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) leaving 2 subgoals.

Let x0 of type ι → ι be given.

Assume H0: ∀ x1 . x1 ∈ 1 ⟶ x0 x1 ∈ 0.

Apply EmptyE with x0 0, not (∀ x1 . x1 ∈ 1 ⟶ ∀ x2 . x2 ∈ 1 ⟶ x0 x1 = x0 x2 ⟶ x1 = x2).

Apply H0 with 0.

The subproof is completed by applying In_0_1.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 : ι → ι . (∀ x2 . x2 ∈ ordsucc x0 ⟶ x1 x2 ∈ x0) ⟶ not (∀ x2 . x2 ∈ ordsucc x0 ⟶ ∀ x3 . x3 ∈ ordsucc x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3).

Let x1 of type ι → ι be given.

Assume H2: ∀ x2 . x2 ∈ ordsucc (ordsucc x0) ⟶ x1 x2 ∈ ordsucc x0.

Assume H3: ∀ x2 . x2 ∈ ordsucc (ordsucc x0) ⟶ ∀ x3 . x3 ∈ ordsucc (ordsucc x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.

Apply xm with ∃ x2 . and (x2 ∈ ordsucc (ordsucc x0)) (x1 x2 = x0), False leaving 2 subgoals.

Assume H4: ∃ x2 . and (x2 ∈ ordsucc (ordsucc x0)) (x1 x2 = x0).

Apply H4 with False.

Let x2 of type ι be given.

Assume H5: (λ x3 . and (x3 ∈ ordsucc (ordsucc x0)) (x1 x3 = x0)) x2.

Apply H5 with False.

Assume H6: x2 ∈ ordsucc (ordsucc x0).

Assume H7: x1 x2 = x0.

Apply H1 with λ x3 . If_i (x2 ⊆ x3) (x1 (ordsucc x3)) (x1 x3) leaving 2 subgoals.

Let x3 of type ι be given.

Assume H8: x3 ∈ ordsucc x0.

Apply xm with x2 ⊆ x3, (λ x4 . If_i (x2 ⊆ x4) (x1 (ordsucc x4)) (x1 x4)) x3 ∈ x0 leaving 2 subgoals.

Assume H9: x2 ⊆ x3.

Apply If_i_1 with x2 ⊆ x3, x1 (ordsucc x3), x1 x3, λ x4 x5 . x5 ∈ x0 leaving 2 subgoals.

The subproof is completed by applying H9.

Claim L10: ordsucc x3 ∈ ...

...

Apply ordsuccE with x0, x1 (ordsucc x3), x1 (ordsucc x3) ∈ x0 leaving 3 subgoals.

Apply H2 with ordsucc x3.

The subproof is completed by applying L10.

Assume H11: x1 (ordsucc x3) ∈ x0.

The subproof is completed by applying H11.

Assume H11: x1 (ordsucc x3) = x0.

Apply FalseE with x1 (ordsucc x3) ∈ x0.

Apply In_irref with x3.

Claim L12: x2 = ordsucc x3

Apply H3 with x2, ordsucc x3 leaving 3 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying L10.

Apply H11 with λ x4 x5 . x1 x2 = x5.

The subproof is completed by applying H7.

Claim L13: x3 ∈ x2

Apply L12 with λ x4 x5 . x3 ∈ x5.

The subproof is completed by applying ordsuccI2 with x3.

Apply H9 with x3.

The subproof is completed by applying L13.

...

■

Proofgold Proof