Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι be given.
Assume H0: ordinal x1.
Let x2 of type ι be given.
Assume H1: x2 ∈ ordsucc x1.
Let x3 of type ι → ο be given.
Assume H2: PNo_strict_upperbd x0 x1 x3.
Let x4 of type ι be given.
Assume H3: x4 ∈ x2.
Let x5 of type ι → ο be given.
Assume H4: PNo_downc x0 x4 x5.
Apply H0 with PNoLt x4 x5 x2 x3.
Assume H5: TransSet x1.
Assume H6: ∀ x6 . x6 ∈ x1 ⟶ TransSet x6.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply H4 with PNoLt x4 x5 x2 x3.
Let x6 of type ι be given.
Assume H12: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (PNoLe x4 x5 x7 x8))) x6.
Apply H12 with PNoLt x4 x5 x2 x3.
Assume H13: ordinal x6.
Assume H14: ∃ x7 : ι → ο . and (x0 x6 x7) (PNoLe x4 x5 x6 x7).
Apply H14 with PNoLt x4 x5 x2 x3.
Let x7 of type ι → ο be given.
Assume H15: (λ x8 : ι → ο . and (x0 x6 x8) (PNoLe x4 x5 x6 x8)) x7.
Apply H15 with PNoLt x4 x5 x2 x3.
Assume H16: x0 x6 x7.
Assume H17: PNoLe x4 x5 x6 x7.
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply PNoLt_trichotomy_or with x4, x2, x5, x3, PNoLt x4 x5 x2 x3 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L8.
Assume H22: or (PNoLt x4 x5 x2 x3) (and (x4 = x2) (PNoEq_ x4 x5 x3)).
Apply H22 with PNoLt x4 x5 x2 x3 leaving 2 subgoals.
Assume H23: PNoLt x4 x5 x2 x3.
The subproof is completed by applying H23.
Assume H23: and (x4 = x2) (PNoEq_ x4 x5 x3).
Apply H23 with PNoLt x4 x5 x2 x3.
Assume H24: x4 = x2.
Apply FalseE with PNoEq_ x4 x5 x3 ⟶ PNoLt x4 x5 x2 x3.
Apply In_irref with x2.
Apply H24 with λ x8 x9 . x8 ∈ x2.
The subproof is completed by applying H3.
Assume H22: PNoLt x2 x3 x4 x5.
Apply FalseE with PNoLt x4 x5 x2 x3.
Apply PNoLtE with x2, x4, x3, x5, False leaving 4 subgoals.
The subproof is completed by applying H22.
Apply binintersect_com with x2, x4, λ x8 x9 . PNoLt_ x9 x3 x5 ⟶ False.
Apply binintersect_Subq_eq_1 with x4, x2, λ x8 x9 . PNoLt_ x9 x3 x5 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L11.
Assume H23: PNoLt_ x4 x3 x5.
Apply H23 with False.
Apply PNoLt_irref with x1, x3, ∀ x8 . (λ x9 . and (x9 ∈ x4) (and (and (PNoEq_ x9 x3 x5) (not (x3 x9))) (x5 x9))) x8 ⟶ False.
Apply PNoLt_tra with x1, x4, x1, x3, x5, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L10.
The subproof is completed by applying H0.
Apply PNoLtI1 with x1, x4, x3, x5.
Apply binintersect_com with x1, x4, λ x8 x9 . PNoLt_ x9 x3 x5.
Apply binintersect_Subq_eq_1 with x4, x1, λ x8 x9 . PNoLt_ x9 x3 x5 leaving 2 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying H23.
The subproof is completed by applying L19.
Assume H23: x2 ∈ x4.
Apply FalseE with ... ⟶ x5 ... ⟶ False.
...
...
■