Let x0 of type ι → (ι → ο) → ο be given.

Let x1 of type ι → (ι → ο) → ο be given.

Assume H0: PNoLt_pwise x0 x1.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Let x3 of type ι → ο be given.

Assume H2: PNo_downc x0 x2 x3.

Let x4 of type ι be given.

Assume H3: ordinal x4.

Let x5 of type ι → ο be given.

Assume H4: PNo_upc x1 x4 x5.

Apply H2 with PNoLt x2 x3 x4 x5.

Let x6 of type ι be given.

Assume H5: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (PNoLe x2 x3 x7 x8))) x6.

Apply H5 with PNoLt x2 x3 x4 x5.

Assume H6: ordinal x6.

Assume H7: ∃ x7 : ι → ο . and (x0 x6 x7) (PNoLe x2 x3 x6 x7).

Apply H7 with PNoLt x2 x3 x4 x5.

Let x7 of type ι → ο be given.

Assume H8: (λ x8 : ι → ο . and (x0 x6 x8) (PNoLe x2 x3 x6 x8)) x7.

Apply H8 with PNoLt x2 x3 x4 x5.

Assume H9: x0 x6 x7.

Assume H10: PNoLe x2 x3 x6 x7.

Apply H4 with PNoLt x2 x3 x4 x5.

Let x8 of type ι be given.

Assume H11: (λ x9 . and (ordinal x9) (∃ x10 : ι → ο . and (x1 x9 x10) (PNoLe x9 x10 x4 x5))) x8.

Apply H11 with PNoLt x2 x3 x4 x5.

Assume H12: ordinal x8.

Assume H13: ∃ x9 : ι → ο . and (x1 x8 x9) (PNoLe x8 x9 x4 x5).

Apply H13 with PNoLt x2 x3 x4 x5.

Let x9 of type ι → ο be given.

Assume H14: (λ x10 : ι → ο . and (x1 x8 x10) (PNoLe x8 x10 x4 x5)) x9.

Apply H14 with PNoLt x2 x3 x4 x5.

Assume H15: x1 x8 x9.

Assume H16: PNoLe x8 x9 x4 x5.

Claim L17: PNoLt x2 x3 x4 x5

...

Apply PNoLt_trichotomy_or with x4, x2, x5, x3, PNoLt x2 x3 x4 x5 leaving 4 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H1.

Assume H18: or (PNoLt x4 x5 x2 x3) (and (x4 = x2) (PNoEq_ x4 x5 x3)).

Apply H18 with PNoLt x2 x3 x4 x5 leaving 2 subgoals.

Assume H19: PNoLt x4 x5 x2 x3.

Apply PNoLt_irref with x2, x3, PNoLt x2 x3 x4 x5.

Apply PNoLt_tra with x2, x4, x2, x3, x5, x3 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

The subproof is completed by applying H1.

The subproof is completed by applying L17.

The subproof is completed by applying H19.

Assume H19: and (x4 = x2) (PNoEq_ x4 x5 x3).

Apply PNoLt_irref with x4, x5, PNoLt x2 x3 x4 x5.

Apply PNoLeLt_tra with x4, x2, x4, x5, x3, x5 leaving 5 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

Apply orIR with PNoLt x4 x5 x2 x3, and (x4 = x2) (PNoEq_ x4 x5 x3).

The subproof is completed by applying H19.

The subproof is completed by applying L17.

Assume H18: PNoLt x2 x3 x4 x5.

The subproof is completed by applying H18.

■

Proofgold Proof