Apply nat_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ x1 ∈ x2 ⟶ add_nat x1 x0 ∈ add_nat x2 x0 leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι be given.

Assume H1: nat_p x1.

Assume H2: x0 ∈ x1.

Apply add_nat_0R with x0, λ x2 x3 . x3 ∈ add_nat x1 0.

Apply add_nat_0R with x1, λ x2 x3 . x0 ∈ x3.

The subproof is completed by applying H2.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ x1 ∈ x2 ⟶ add_nat x1 x0 ∈ add_nat x2 x0.

Let x1 of type ι be given.

Assume H2: nat_p x1.

Let x2 of type ι be given.

Assume H3: nat_p x2.

Assume H4: x1 ∈ x2.

Apply add_nat_SR with x1, x0, λ x3 x4 . x4 ∈ add_nat x2 (ordsucc x0) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply add_nat_SR with x2, x0, λ x3 x4 . ordsucc (add_nat x1 x0) ∈ x4 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply add_nat_SL with x1, x0, λ x3 x4 . x3 ∈ ordsucc (add_nat x2 x0) leaving 3 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H0.

Apply add_nat_SL with x2, x0, λ x3 x4 . add_nat (ordsucc x1) x0 ∈ x3 leaving 3 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H0.

Claim L5: ordinal x1

Apply nat_p_ordinal with x1.

The subproof is completed by applying H2.

Claim L6: ordinal x2

Apply nat_p_ordinal with x2.

The subproof is completed by applying H3.

Claim L7: ordinal (ordsucc x2)

Apply ordinal_ordsucc with x2.

The subproof is completed by applying L6.

Apply H1 with ordsucc x1, ordsucc x2 leaving 3 subgoals.

Apply nat_ordsucc with x1.

The subproof is completed by applying H2.

Apply nat_ordsucc with x2.

The subproof is completed by applying H3.

Apply nat_ordsucc_in_ordsucc with x2, x1 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

■

Proofgold Proof