Step | Hyp | Ref
| Expression |
1 | | ramlb.c |
. . . . 5
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) |
2 | | ramlb.m |
. . . . . 6
β’ (π β π β
β0) |
3 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β π β
β0) |
4 | | ramlb.r |
. . . . . 6
β’ (π β π
β π) |
5 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β π
β π) |
6 | | ramlb.f |
. . . . . 6
β’ (π β πΉ:π
βΆβ0) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β πΉ:π
βΆβ0) |
8 | | ramlb.s |
. . . . . . 7
β’ (π β π β
β0) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ (π Ramsey πΉ) β€ π) β π β
β0) |
10 | | simpr 486 |
. . . . . 6
β’ ((π β§ (π Ramsey πΉ) β€ π) β (π Ramsey πΉ) β€ π) |
11 | | ramubcl 16951 |
. . . . . 6
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ (π β β0
β§ (π Ramsey πΉ) β€ π)) β (π Ramsey πΉ) β
β0) |
12 | 3, 5, 7, 9, 10, 11 | syl32anc 1379 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β (π Ramsey πΉ) β
β0) |
13 | | fzfid 13938 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β (1...π) β Fin) |
14 | | hashfz1 14306 |
. . . . . . . 8
β’ (π β β0
β (β―β(1...π)) = π) |
15 | 8, 14 | syl 17 |
. . . . . . 7
β’ (π β (β―β(1...π)) = π) |
16 | 15 | breq2d 5161 |
. . . . . 6
β’ (π β ((π Ramsey πΉ) β€ (β―β(1...π)) β (π Ramsey πΉ) β€ π)) |
17 | 16 | biimpar 479 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β (π Ramsey πΉ) β€ (β―β(1...π))) |
18 | | ramlb.g |
. . . . . 6
β’ (π β πΊ:((1...π)πΆπ)βΆπ
) |
19 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ (π Ramsey πΉ) β€ π) β πΊ:((1...π)πΆπ)βΆπ
) |
20 | 1, 3, 5, 7, 12, 13, 17, 19 | rami 16948 |
. . . 4
β’ ((π β§ (π Ramsey πΉ) β€ π) β βπ β π
βπ₯ β π« (1...π)((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘πΊ β {π}))) |
21 | | elpwi 4610 |
. . . . . . . . 9
β’ (π₯ β π« (1...π) β π₯ β (1...π)) |
22 | | ramlb.i |
. . . . . . . . . . 11
β’ ((π β§ (π β π
β§ π₯ β (1...π))) β ((π₯πΆπ) β (β‘πΊ β {π}) β (β―βπ₯) < (πΉβπ))) |
23 | 22 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β ((π₯πΆπ) β (β‘πΊ β {π}) β (β―βπ₯) < (πΉβπ))) |
24 | | fzfid 13938 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β (1...π) β Fin) |
25 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β π₯ β (1...π)) |
26 | 24, 25 | ssfid 9267 |
. . . . . . . . . . . . 13
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β π₯ β Fin) |
27 | | hashcl 14316 |
. . . . . . . . . . . . 13
β’ (π₯ β Fin β
(β―βπ₯) β
β0) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β (β―βπ₯) β
β0) |
29 | 28 | nn0red 12533 |
. . . . . . . . . . 11
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β (β―βπ₯) β β) |
30 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β π
β§ π₯ β (1...π)) β π β π
) |
31 | | ffvelcdm 7084 |
. . . . . . . . . . . . 13
β’ ((πΉ:π
βΆβ0 β§ π β π
) β (πΉβπ) β
β0) |
32 | 7, 30, 31 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β (πΉβπ) β
β0) |
33 | 32 | nn0red 12533 |
. . . . . . . . . . 11
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β (πΉβπ) β β) |
34 | 29, 33 | ltnled 11361 |
. . . . . . . . . 10
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β ((β―βπ₯) < (πΉβπ) β Β¬ (πΉβπ) β€ (β―βπ₯))) |
35 | 23, 34 | sylibd 238 |
. . . . . . . . 9
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β (1...π))) β ((π₯πΆπ) β (β‘πΊ β {π}) β Β¬ (πΉβπ) β€ (β―βπ₯))) |
36 | 21, 35 | sylanr2 682 |
. . . . . . . 8
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β π« (1...π))) β ((π₯πΆπ) β (β‘πΊ β {π}) β Β¬ (πΉβπ) β€ (β―βπ₯))) |
37 | 36 | con2d 134 |
. . . . . . 7
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β π« (1...π))) β ((πΉβπ) β€ (β―βπ₯) β Β¬ (π₯πΆπ) β (β‘πΊ β {π}))) |
38 | | imnan 401 |
. . . . . . 7
β’ (((πΉβπ) β€ (β―βπ₯) β Β¬ (π₯πΆπ) β (β‘πΊ β {π})) β Β¬ ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘πΊ β {π}))) |
39 | 37, 38 | sylib 217 |
. . . . . 6
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β π« (1...π))) β Β¬ ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘πΊ β {π}))) |
40 | 39 | pm2.21d 121 |
. . . . 5
β’ (((π β§ (π Ramsey πΉ) β€ π) β§ (π β π
β§ π₯ β π« (1...π))) β (((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘πΊ β {π})) β Β¬ (π Ramsey πΉ) β€ π)) |
41 | 40 | rexlimdvva 3212 |
. . . 4
β’ ((π β§ (π Ramsey πΉ) β€ π) β (βπ β π
βπ₯ β π« (1...π)((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘πΊ β {π})) β Β¬ (π Ramsey πΉ) β€ π)) |
42 | 20, 41 | mpd 15 |
. . 3
β’ ((π β§ (π Ramsey πΉ) β€ π) β Β¬ (π Ramsey πΉ) β€ π) |
43 | 42 | pm2.01da 798 |
. 2
β’ (π β Β¬ (π Ramsey πΉ) β€ π) |
44 | 8 | nn0red 12533 |
. . . 4
β’ (π β π β β) |
45 | 44 | rexrd 11264 |
. . 3
β’ (π β π β
β*) |
46 | | ramxrcl 16950 |
. . . 4
β’ ((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β (π Ramsey πΉ) β
β*) |
47 | 2, 4, 6, 46 | syl3anc 1372 |
. . 3
β’ (π β (π Ramsey πΉ) β
β*) |
48 | | xrltnle 11281 |
. . 3
β’ ((π β β*
β§ (π Ramsey πΉ) β β*)
β (π < (π Ramsey πΉ) β Β¬ (π Ramsey πΉ) β€ π)) |
49 | 45, 47, 48 | syl2anc 585 |
. 2
β’ (π β (π < (π Ramsey πΉ) β Β¬ (π Ramsey πΉ) β€ π)) |
50 | 43, 49 | mpbird 257 |
1
β’ (π β π < (π Ramsey πΉ)) |