Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u6.
Let x1 of type ι be given.
Assume H1: x1 ∈ u6.
Let x2 of type ι be given.
Assume H2: x2 ∈ u6.
Let x3 of type ι be given.
Assume H3: x3 ∈ u6.
Assume H4: not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3).
Claim L5: ordinal x0
Apply nat_p_ordinal with x0.
Apply nat_p_trans with u6, x0 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying H0.
Claim L6: ordinal x1
Apply nat_p_ordinal with x1.
Apply nat_p_trans with u6, x1 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying H1.
Claim L7: ordinal x2
Apply nat_p_ordinal with x2.
Apply nat_p_trans with u6, x2 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying H2.
Claim L8: ordinal x3
Apply nat_p_ordinal with x3.
Apply nat_p_trans with u6, x3 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying H3.
Apply ordinal_trichotomy_or_impred with x0, x2, or (5fab1.. x0 x1 x2 x3) (5fab1.. x2 x3 x0 x1) leaving 5 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L7.
Assume H9: x0 ∈ x2.
Apply orIL with 5fab1.. x0 x1 x2 x3, 5fab1.. x2 x3 x0 x1.
Apply orIL with x0 ∈ x2, and (x0 = x2) (x1 ∈ x3).
The subproof is completed by applying H9.
Assume H9: x0 = x2.
Apply ordinal_trichotomy_or_impred with x1, x3, or (5fab1.. x0 x1 x2 x3) (5fab1.. x2 x3 x0 x1) leaving 5 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L8.
Assume H10: x1 ∈ x3.
Apply orIL with 5fab1.. x0 x1 x2 x3, 5fab1.. x2 x3 x0 x1.
Apply orIR with x0 ∈ x2, and (x0 = x2) (x1 ∈ x3).
Apply andI with x0 = x2, x1 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Assume H10: x1 = x3.
Apply FalseE with or (5fab1.. x0 x1 x2 x3) (5fab1.. x2 x3 x0 x1).
Apply H4.
Apply H9 with λ x4 x5 . TwoRamseyGraph_4_6_35_a x0 x1 x4 x3.
Apply H10 with λ x4 x5 . TwoRamseyGraph_4_6_35_a x0 x1 x0 x4.
Apply unknownprop_c92c0588de1ba6f1a5352aaa897a2358c5ed2f086efe24dfed8c7d8036084229 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H10: x3 ∈ x1.
Apply orIR with 5fab1.. x0 x1 x2 x3, 5fab1.. x2 x3 x0 x1.
Apply orIR with x2 ∈ x0, and (x2 = x0) (x3 ∈ x1).
Apply andI with x2 = x0, x3 ∈ x1 leaving 2 subgoals.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H9 with λ x5 x6 . x4 x6 x5.
The subproof is completed by applying H10.
Assume H9: x2 ∈ x0.
Apply orIR with 5fab1.. x0 x1 x2 x3, 5fab1.. x2 x3 x0 x1.
Apply orIL with x2 ∈ x0, and (x2 = x0) (x3 ∈ x1).
The subproof is completed by applying H9.
■