Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ο be given.

Let x3 of type ι → ο be given.

Apply unknownprop_b73af4382aa2130f443f8d39ac8ce95cd65e1e810ddcea4fbd727ebc17c2f4ca with λ x4 x5 : ι → (ι → ο) → ι → (ι → ο) → ο . x5 x0 x2 x1 x3 ⟶ ∀ x6 : ο . (PNoLt_ (binintersect x0 x1) x2 x3 ⟶ x6) ⟶ (In x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x6) ⟶ (In x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x6) ⟶ x6.

Assume H0: (λ x4 . λ x5 : ι → ο . λ x6 . λ x7 : ι → ο . or (or (PNoLt_ (binintersect x4 x6) x5 x7) (and (and (In x4 x6) (PNoEq_ x4 x5 x7)) (x7 x4))) (and (and (In x6 x4) (PNoEq_ x6 x5 x7)) (not (x5 x6)))) x0 x2 x1 x3.

Let x4 of type ο be given.

Assume H1: PNoLt_ (binintersect x0 x1) x2 x3 ⟶ x4.

Assume H2: In x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x4.

Assume H3: In x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x4.

Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with PNoLt_ (binintersect x0 x1) x2 x3, and (and (In x0 x1) (PNoEq_ x0 x2 x3)) (x3 x0), and (and (In x1 x0) (PNoEq_ x1 x2 x3)) (not (x2 x1)), x4 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Assume H4: and (and (In x0 x1) (PNoEq_ x0 x2 x3)) (x3 x0).

Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with In x0 x1, PNoEq_ x0 x2 x3, x3 x0, x4 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H2.

Assume H4: and (and (In x1 x0) (PNoEq_ x1 x2 x3)) (not (x2 x1)).

Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with In x1 x0, PNoEq_ x1 x2 x3, not (x2 x1), x4 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H3.

■

Proofgold Proof