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

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

Assume H0: 3f2f5.. x0 x1.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Let x3 of type ι → ο be given.

Apply unknownprop_10b092fb3ef85ea31ee360e7dc788511bcc4358b1df6c96ac348bc4af6827002 with x0, x2, x3, ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . PNo_upc x1 x4 x5 ⟶ PNoLt x2 x3 x4 x5.

Let x4 of type ι be given.

Assume H2: ordinal x4.

Let x5 of type ι → ο be given.

Assume H3: x0 x4 x5.

Assume H4: PNoLe x2 x3 x4 x5.

Let x6 of type ι be given.

Assume H5: ordinal x6.

Let x7 of type ι → ο be given.

Apply unknownprop_6d8aab3a07e18c6be73ac4f468e0bb765aa8d07746b2e7910d23f976851c109f with x1, x6, x7, PNoLt x2 x3 x6 x7.

Let x8 of type ι be given.

Assume H6: ordinal x8.

Let x9 of type ι → ο be given.

Assume H7: x1 x8 x9.

Assume H8: PNoLe x8 x9 x6 x7.

Claim L9: PNoLt x2 x3 x6 x7

Apply unknownprop_e1eeb1ab78949417ed3beb1b848798226da26b1dc30d0d60a989f8c7ea33fd62 with x2, x4, x6, x3, x5, x7 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H5.

The subproof is completed by applying H4.

Apply unknownprop_38fe47c02c45b572d571f0ab8bb77c5704469fbed9372485a9c3b22772d10fe0 with x4, x8, x6, x5, x9, x7 leaving 5 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H6.

The subproof is completed by applying H5.

Apply H0 with x4, x5, x8, x9 leaving 4 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

Apply unknownprop_b79cb1702e8ed87da3fa15a463d1286cd0e769d607a361b393d7ac2b561606df with x6, x2, x7, x3, PNoLt x2 x3 x6 x7 leaving 5 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H1.

Assume H10: PNoLt x6 x7 x2 x3.

Apply FalseE with PNoLt x2 x3 x6 x7.

Apply unknownprop_538b32da6e929848b1738bc95c54e7b85ed02786c342b641da55ecd1e295e69b with x2, x3.

Apply unknownprop_6bb26b25b4b138d2d5816191bcd658afb4958cf8c28d95f1e213b943c7319173 with x2, x6, x2, x3, x7, x3 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H5.

The subproof is completed by applying H1.

The subproof is completed by applying L9.

The subproof is completed by applying H10.

Assume H10: x6 = x2.

Assume H11: PNoEq_ x6 x7 x3.

Apply FalseE with PNoLt x2 x3 x6 x7.

Apply unknownprop_538b32da6e929848b1738bc95c54e7b85ed02786c342b641da55ecd1e295e69b with x6, x7.

Apply unknownprop_e1eeb1ab78949417ed3beb1b848798226da26b1dc30d0d60a989f8c7ea33fd62 with x6, x2, x6, x7, x3, x7 leaving 5 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H1.

The subproof is completed by applying H5.

Apply H10 with λ x10 x11 . PNoLe x6 x7 x10 x3.

Apply unknownprop_a390ce3b156cb5dba6e2555585ed1d8e112537b24a7e90ed34a8f7f5ef39d7f0 with x6, x7, x3.

The subproof is completed by applying H11.

The subproof is completed by applying L9.

Assume H10: PNoLt x2 x3 x6 x7.

The subproof is completed by applying H10.

■

Proofgold Proof