Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Assume H2: PNoLt x0 x2 x1 x3.
Assume H3: PNoEq_ x1 x3 x4.
Apply PNoLtE with x0, x1, x2, x3, PNoLt x0 x2 x1 x4 leaving 4 subgoals.
The subproof is completed by applying H2.
Assume H4: PNoLt_ (binintersect x0 x1) x2 x3.
Apply H4 with PNoLt x0 x2 x1 x4.
Let x5 of type ι be given.
Assume H5: (λ x6 . and (x6 ∈ binintersect x0 x1) (and (and (PNoEq_ x6 x2 x3) (not (x2 x6))) (x3 x6))) x5.
Apply H5 with PNoLt x0 x2 x1 x4.
Assume H6: x5 ∈ binintersect x0 x1.
Apply binintersectE with x0, x1, x5, and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5) ⟶ PNoLt x0 x2 x1 x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: x5 ∈ x0.
Assume H8: x5 ∈ x1.
Assume H9: and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5).
Apply H9 with PNoLt x0 x2 x1 x4.
Assume H10: and (PNoEq_ x5 x2 x3) (not (x2 x5)).
Apply H10 with x3 x5 ⟶ PNoLt x0 x2 x1 x4.
Assume H11: PNoEq_ x5 x2 x3.
Assume H12: not (x2 x5).
Assume H13: x3 x5.
Apply PNoLtI1 with x0, x1, x2, x4.
Let x6 of type ο be given.
Assume H14: ∀ x7 . and (x7 ∈ binintersect x0 x1) (and (and (PNoEq_ x7 x2 x4) (not (x2 x7))) (x4 x7)) ⟶ x6.
Apply H14 with x5.
Apply andI with x5 ∈ binintersect x0 x1, and (and (PNoEq_ x5 x2 x4) (not (x2 x5))) (x4 x5) leaving 2 subgoals.
The subproof is completed by applying H6.
Apply and3I with PNoEq_ x5 x2 x4, not (x2 x5), x4 x5 leaving 3 subgoals.
Apply PNoEq_tra_ with x5, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply PNoEq_antimon_ with x3, x4, x1, x5 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H8.
The subproof is completed by applying H3.
The subproof is completed by applying H12.
Apply iffEL with x3 x5, x4 x5 leaving 2 subgoals.
Apply H3 with x5.
The subproof is completed by applying H8.
The subproof is completed by applying H13.
Assume H4: x0 ∈ x1.
Assume H5: PNoEq_ x0 x2 x3.
Assume H6: x3 x0.
Apply PNoLtI2 with x0, x1, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply PNoEq_tra_ with x0, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply PNoEq_antimon_ with x3, x4, x1, x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Apply iffEL with x3 x0, x4 x0 leaving 2 subgoals.
Apply H3 with x0.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Assume H4: x1 ∈ x0.
Assume H5: PNoEq_ x1 x2 x3.
Assume H6: not (x2 x1).
Apply PNoLtI3 with x0, x1, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply PNoEq_tra_ with x1, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
■