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 H2 with
and (x0 = x1) (PNoEq_ x0 x2 x3) leaving 2 subgoals.
Assume H4:
PNoLt x0 x2 x1 x3.
Apply FalseE with
and (x0 = x1) (PNoEq_ x0 x2 x3).
Apply H3 with
False leaving 2 subgoals.
Assume H5:
PNoLt x1 x3 x0 x2.
Apply PNoLt_irref with
x0,
x2.
Apply PNoLt_tra with
x0,
x1,
x0,
x2,
x3,
x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H5 with
False.
Assume H6: x1 = x0.
Apply PNoLtE with
x0,
x1,
x2,
x3,
False leaving 4 subgoals.
The subproof is completed by applying H4.
Apply H8 with
False.
Let x4 of type ι be given.
Apply H9 with
False.
Apply binintersectE with
x0,
x1,
x4,
and (and (PNoEq_ x4 x2 x3) (not (x2 x4))) (x3 x4) ⟶ False leaving 2 subgoals.
The subproof is completed by applying H10.
Assume H11: x4 ∈ x0.
Assume H12: x4 ∈ x1.
Apply H13 with
False.
Apply H14 with
x3 x4 ⟶ False.
Assume H17: x3 x4.
Apply H16.
Apply iffEL with
x3 x4,
x2 x4 leaving 2 subgoals.
Apply H7 with
x4.
The subproof is completed by applying H12.
The subproof is completed by applying H17.
Assume H8: x0 ∈ x1.
Assume H10: x3 x0.
Apply In_irref with
x0.
Apply H6 with
λ x4 x5 . x0 ∈ x4.
The subproof is completed by applying H8.
Assume H8: x1 ∈ x0.
Apply In_irref with
x0.
Apply H6 with
λ x4 x5 . x4 ∈ x0.
The subproof is completed by applying H8.
The subproof is completed by applying H4.