Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u12.
Assume H1: atleastp u5 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ not (and (TwoRamseyGraph_3_6_17 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)).
Apply unknownprop_82a4043338dce48d58934c215ccdbe85be545db6869ac125d5e92b153cac28bb with x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3.
Assume H6: TwoRamseyGraph_3_6_17 x1 x2.
Apply H2 with x1, x2 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply andI with TwoRamseyGraph_3_6_17 x1 x2, x1 = x2 ⟶ ∀ x3 : ο . x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
■