Let x0 of type ι → ο be given.

Let x1 of type ι → ο be given.

Apply unknownprop_a136f966a5f32c42970eaa74da643e650a33010b04dec952965730ae1dedc69c 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 . In x3 x2 ⟶ or (or (PNoLt_ x3 x0 x1) (PNoEq_ x3 x0 x1)) (PNoLt_ x3 x1 x0).

Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 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 unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1), PNoLt_ x2 x1 x0.

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

The subproof is completed by applying H2.

Apply unknownprop_ee0b4b64aba8e6af97035d72b359ab8e1ae1e5e06024c58477c9410cad648356 with λ x3 x4 : ι → (ι → ο) → (ι → ο) → ο . not (x4 x2 x0 x1) ⟶ or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).

Assume H2: not ((λ x3 . λ x4 x5 : ι → ο . ∀ x6 . In x6 x3 ⟶ iff (x4 x6) (x5 x6)) 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 (In x3 x2 ⟶ iff (x0 x3) (x1 x3)).

Claim L5: ...

...

Apply andE with In x3 x2, not (iff (x0 x3) (x1 x3)), or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.

The subproof is completed by applying L5.

Assume H6: In x3 x2.

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

Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with PNoLt_ x3 x0 x1, PNoEq_ x3 x0 x1, PNoLt_ x3 x1 x0, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 4 subgoals.

Apply H1 with x3.

The subproof is completed by applying H6.

Assume H8: PNoLt_ x3 x0 x1.

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

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

Apply unknownprop_6df6296e43f9bca3c044b15e64641a9a31579aac9d81b18192c24adabec23296 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 H8.

Assume H8: PNoEq_ x3 x0 x1.

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

Assume H9: x0 x3.

...

■

Proofgold Proof