Let x0 of type ι be given.

Assume H0: nat_p x0.

Apply H0 with λ x1 . ∀ x2 . x2 ∈ x1 ⟶ ordsucc x2 ∈ ordsucc x1 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H1: x1 ∈ 0.

Apply FalseE with ordsucc x1 ∈ 1.

Apply EmptyE with x1.

The subproof is completed by applying H1.

Let x1 of type ι be given.

Assume H1: ∀ x2 . x2 ∈ x1 ⟶ ordsucc x2 ∈ ordsucc x1.

Let x2 of type ι be given.

Assume H2: x2 ∈ ordsucc x1.

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

The subproof is completed by applying H2.

Assume H3: x2 ∈ x1.

Claim L4: ordsucc x2 ∈ ordsucc x1

Apply H1 with x2.

The subproof is completed by applying H3.

Apply ordsuccI1 with ordsucc x1, ordsucc x2.

The subproof is completed by applying L4.

Assume H3: x2 = x1.

Apply H3 with λ x3 x4 . ordsucc x4 ∈ ordsucc (ordsucc x1).

The subproof is completed by applying ordsuccI2 with ordsucc x1.

■

Proofgold Proof