Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Assume H0: ordinal x2.
Let x3 of type ι → ο be given.
Assume H1: PNo_rel_strict_split_imv x0 x1 x2 x3.
Claim L2: ...
...
Apply H1 with PNo_strict_imv x0 x1 x2 x3.
Assume H3: PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Assume H4: PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)).
Apply H3 with PNo_strict_imv x0 x1 x2 x3.
Assume H5: PNo_rel_strict_upperbd x0 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Assume H6: PNo_rel_strict_lowerbd x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Apply H4 with PNo_strict_imv x0 x1 x2 x3.
Assume H7: PNo_rel_strict_upperbd x0 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)).
Assume H8: PNo_rel_strict_lowerbd x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)).
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Apply andI with PNo_strict_upperbd x0 x2 x3, PNo_strict_lowerbd x1 x2 x3 leaving 2 subgoals.
Let x4 of type ι be given.
Assume H13: ordinal x4.
Let x5 of type ι → ο be given.
Assume H14: x0 x4 x5.
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Apply PNoLt_trichotomy_or with x2, x4, x3, x5, PNoLt x4 x5 x2 x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H13.
Assume H18: or (PNoLt x2 x3 x4 x5) (and (x2 = x4) (PNoEq_ x2 x3 x5)).
Apply H18 with PNoLt x4 x5 x2 x3 leaving 2 subgoals.
Assume H19: PNoLt x2 x3 x4 x5.
Apply PNoLtE with x2, x4, x3, x5, PNoLt x4 x5 x2 x3 leaving 4 subgoals.
The subproof is completed by applying H19.
Assume H20: PNoLt_ (binintersect x2 x4) x3 x5.
Apply H20 with PNoLt x4 x5 x2 x3.
Let x6 of type ι be given.
Assume H21: (λ x7 . and (x7 ∈ binintersect x2 x4) (and (and (PNoEq_ x7 x3 x5) (not (x3 x7))) (x5 x7))) x6.
Apply H21 with PNoLt x4 x5 x2 x3.
Assume H22: x6 ∈ binintersect x2 x4.
Assume H23: and (and (PNoEq_ x6 x3 x5) (not (x3 x6))) (x5 x6).
Apply H23 with PNoLt x4 x5 x2 x3.
Assume H24: and (PNoEq_ x6 x3 x5) (not (x3 x6)).
Apply H24 with x5 x6 ⟶ PNoLt x4 x5 x2 x3.
Assume H25: PNoEq_ x6 x3 x5.
Assume H26: not (x3 x6).
Assume H27: x5 x6.
Apply FalseE with PNoLt x4 x5 x2 x3.
Apply binintersectE with x2, x4, x6, False leaving 2 subgoals.
The subproof is completed by applying H22.
Assume H28: x6 ∈ x2.
Assume H29: x6 ∈ ....
...
...
...
...
...
...
■