Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’ (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) |
2 | | simpl1 1192 |
. . . 4
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β π β β) |
3 | 2 | nnnn0d 12481 |
. . 3
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β π β
β0) |
4 | | simpl2 1193 |
. . 3
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β π
β π) |
5 | | simpl3 1194 |
. . 3
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β πΉ:π
βΆβ0) |
6 | | 0nn0 12436 |
. . . 4
β’ 0 β
β0 |
7 | 6 | a1i 11 |
. . 3
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β 0 β
β0) |
8 | | simplrl 776 |
. . . 4
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β πΆ β π
) |
9 | | 0elpw 5315 |
. . . . 5
β’ β
β π« π |
10 | 9 | a1i 11 |
. . . 4
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β β
β π« π ) |
11 | | simplrr 777 |
. . . . 5
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β (πΉβπΆ) = 0) |
12 | | 0le0 12262 |
. . . . 5
β’ 0 β€
0 |
13 | 11, 12 | eqbrtrdi 5148 |
. . . 4
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β (πΉβπΆ) β€ 0) |
14 | | simpll1 1213 |
. . . . . 6
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β π β β) |
15 | 1 | 0hashbc 16887 |
. . . . . 6
β’ (π β β β
(β
(π β V, π β β0
β¦ {π β π«
π β£
(β―βπ) = π})π) = β
) |
16 | 14, 15 | syl 17 |
. . . . 5
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β (β
(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) = β
) |
17 | | 0ss 4360 |
. . . . 5
β’ β
β (β‘π β {πΆ}) |
18 | 16, 17 | eqsstrdi 4002 |
. . . 4
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β (β
(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ})) |
19 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΆ β (πΉβπ) = (πΉβπΆ)) |
20 | 19 | breq1d 5119 |
. . . . . 6
β’ (π = πΆ β ((πΉβπ) β€ (β―βπ₯) β (πΉβπΆ) β€ (β―βπ₯))) |
21 | | sneq 4600 |
. . . . . . . 8
β’ (π = πΆ β {π} = {πΆ}) |
22 | 21 | imaeq2d 6017 |
. . . . . . 7
β’ (π = πΆ β (β‘π β {π}) = (β‘π β {πΆ})) |
23 | 22 | sseq2d 3980 |
. . . . . 6
β’ (π = πΆ β ((π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {π}) β (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ}))) |
24 | 20, 23 | anbi12d 632 |
. . . . 5
β’ (π = πΆ β (((πΉβπ) β€ (β―βπ₯) β§ (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {π})) β ((πΉβπΆ) β€ (β―βπ₯) β§ (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ})))) |
25 | | fveq2 6846 |
. . . . . . . 8
β’ (π₯ = β
β
(β―βπ₯) =
(β―ββ
)) |
26 | | hash0 14276 |
. . . . . . . 8
β’
(β―ββ
) = 0 |
27 | 25, 26 | eqtrdi 2789 |
. . . . . . 7
β’ (π₯ = β
β
(β―βπ₯) =
0) |
28 | 27 | breq2d 5121 |
. . . . . 6
β’ (π₯ = β
β ((πΉβπΆ) β€ (β―βπ₯) β (πΉβπΆ) β€ 0)) |
29 | | oveq1 7368 |
. . . . . . 7
β’ (π₯ = β
β (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) = (β
(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)) |
30 | 29 | sseq1d 3979 |
. . . . . 6
β’ (π₯ = β
β ((π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ}) β (β
(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ}))) |
31 | 28, 30 | anbi12d 632 |
. . . . 5
β’ (π₯ = β
β (((πΉβπΆ) β€ (β―βπ₯) β§ (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ})) β ((πΉβπΆ) β€ 0 β§ (β
(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ})))) |
32 | 24, 31 | rspc2ev 3594 |
. . . 4
β’ ((πΆ β π
β§ β
β π« π β§ ((πΉβπΆ) β€ 0 β§ (β
(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {πΆ}))) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {π}))) |
33 | 8, 10, 13, 18, 32 | syl112anc 1375 |
. . 3
β’ ((((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β§ (0 β€ (β―βπ ) β§ π:(π (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π)βΆπ
)) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯(π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π})π) β (β‘π β {π}))) |
34 | 1, 3, 4, 5, 7, 33 | ramub 16893 |
. 2
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β (π Ramsey πΉ) β€ 0) |
35 | | ramubcl 16898 |
. . . 4
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ (0 β
β0 β§ (π Ramsey πΉ) β€ 0)) β (π Ramsey πΉ) β
β0) |
36 | 3, 4, 5, 7, 34, 35 | syl32anc 1379 |
. . 3
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β (π Ramsey πΉ) β
β0) |
37 | | nn0le0eq0 12449 |
. . 3
β’ ((π Ramsey πΉ) β β0 β ((π Ramsey πΉ) β€ 0 β (π Ramsey πΉ) = 0)) |
38 | 36, 37 | syl 17 |
. 2
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β ((π Ramsey πΉ) β€ 0 β (π Ramsey πΉ) = 0)) |
39 | 34, 38 | mpbid 231 |
1
β’ (((π β β β§ π
β π β§ πΉ:π
βΆβ0) β§ (πΆ β π
β§ (πΉβπΆ) = 0)) β (π Ramsey πΉ) = 0) |