Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H0: x3 ∈ ordsucc (ordsucc x0).

Assume H1: ordsucc x4 ∈ ordsucc (ordsucc x0).

Assume H2: not (x2 ⊆ x3).

Assume H3: x2 ⊆ x4.

Assume H4: x1 x3 = x1 (ordsucc x4).

Assume H5: x3 = ordsucc x4.

Apply H2.

Let x5 of type ι be given.

Assume H6: x5 ∈ x2.

Apply H5 with λ x6 x7 . x5 ∈ x7.

Apply ordsuccI1 with x4, x5.

Apply H3 with x5.

The subproof is completed by applying H6.

■