Let x0 of type ι → ο be given.

Let x1 of type ι → ο be given.

Apply ordinal_ind with λ x2 . or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).

Let x2 of type ι be given.

Assume H0: ordinal x2.

Assume H1: ∀ x3 . x3 ∈ x2 ⟶ or (or (PNoLt_ x3 x0 x1) (PNoEq_ x3 x0 x1)) (PNoLt_ x3 x1 x0).

Apply xm with PNoEq_ x2 x0 x1, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.

Assume H2: PNoEq_ x2 x0 x1.

Apply orIL with or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1), PNoLt_ x2 x1 x0.

Apply orIR with PNoLt_ x2 x0 x1, PNoEq_ x2 x0 x1.

The subproof is completed by applying H2.

Assume H2: not (PNoEq_ x2 x0 x1).

Claim L3: ...

...

Apply L3 with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).

Let x3 of type ι be given.

Assume H4: not (x3 ∈ x2 ⟶ iff (x0 x3) (x1 x3)).

Claim L5: ...

...

Apply L5 with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).

Assume H6: x3 ∈ x2.

Assume H7: not (iff (x0 x3) (x1 x3)).

Apply H1 with x3, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 3 subgoals.

The subproof is completed by applying H6.

Assume H8: or (PNoLt_ x3 x0 x1) (PNoEq_ x3 x0 x1).

Apply H8 with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.

Assume H9: PNoLt_ x3 x0 x1.

Apply orIL with or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1), PNoLt_ x2 x1 x0.

Apply orIL with PNoLt_ x2 x0 x1, PNoEq_ x2 x0 x1.

Apply PNoLt_mon_ with x0, x1, x2, x3 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H6.

The subproof is completed by applying H9.

Assume H9: PNoEq_ x3 x0 x1.

Apply xm with x0 x3, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.

Assume H10: x0 x3.

Apply xm with x1 x3, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.

Assume H11: x1 x3.

Apply FalseE with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 ...)) ....

...

■

Proofgold Proof