Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: x0 u12 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x13.
Assume H1: x0 u13 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x14.
Assume H2: x0 u14 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x15.
Assume H3: x0 u15 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x16.
Assume H4: x0 u16 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x17.
Let x1 of type ι → ι → ο be given.
Assume H5: ∀ x2 x3 . (TwoRamseyGraph_3_6_Church17 (x0 x2) (x0 x3) = λ x4 x5 . x4) ⟶ x1 x2 x3.
Assume H6: ∀ x2 . x2 ⊆ u12 ⟶ atleastp u5 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x1 x3 x4)).
Assume H7: ∀ x2 . x2 ⊆ u16 ⟶ atleastp u6 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x1 x3 x4)).
Let x2 of type ι be given.
Assume H8: x2 ⊆ u17.
Assume H9: atleastp u6 x2.
Assume H10: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x1 x3 x4).
Apply xm with u16 ∈ x2, False leaving 2 subgoals.
Assume H11: u16 ∈ x2.
Claim L12: ...
...
Claim L13: atleastp u5 (binintersect x2 u16)
Apply H9 with atleastp u5 (binintersect x2 u16).
Let x3 of type ι → ι be given.
Assume H13: inj u6 x2 x3.
Apply H13 with atleastp u5 (binintersect x2 u16).
Assume H14: ∀ x4 . x4 ∈ u6 ⟶ x3 x4 ∈ x2.
Assume H15: ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Claim L16: ...
...
Claim L17: ...
...
Let x4 of type ο be given.
Assume H18: ∀ x5 : ι → ι . inj u5 (binintersect x2 u16) x5 ⟶ x4.
Apply H18 with λ x5 . x3 ((λ x6 . If_i (∃ x7 . and (x7 ∈ ordsucc x6) (x3 x7 = u16)) (ordsucc x6) x6) x5).
Apply andI with ∀ x5 . x5 ∈ u5 ⟶ (λ x6 . x3 ((λ x7 . If_i (∃ x8 . and (x8 ∈ ordsucc x7) (x3 x8 = u16)) (ordsucc x7) x7) x6)) x5 ∈ binintersect x2 u16, ∀ x5 . ... ⟶ ∀ x6 . ... ⟶ (λ x7 . x3 ((λ x8 . If_i (∃ x9 . and (x9 ∈ ordsucc x8) (x3 x9 = u16)) (ordsucc x8) x8) x7)) x5 = (λ x7 . x3 ((λ x8 . If_i (∃ x9 . and (x9 ∈ ordsucc x8) (x3 x9 = ...)) ... ...) ...)) ... ⟶ x5 = x6 leaving 2 subgoals.
...
...
Apply H6 with binintersect x2 u16 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
Let x3 of type ι be given.
Assume H14: x3 ∈ binintersect x2 u16.
Let x4 of type ι be given.
Assume H15: x4 ∈ binintersect x2 u16.
Apply H10 with x3, x4 leaving 2 subgoals.
Apply binintersectE1 with x2, u16, x3.
The subproof is completed by applying H14.
Apply binintersectE1 with x2, u16, x4.
The subproof is completed by applying H15.
...
■