Step | Hyp | Ref
| Expression |
1 | | ffn 6718 |
. . . . . . . 8
β’ (πΉ:π
βΆβ0 β πΉ Fn π
) |
2 | | dffn4 6812 |
. . . . . . . 8
β’ (πΉ Fn π
β πΉ:π
βontoβran πΉ) |
3 | 1, 2 | sylib 217 |
. . . . . . 7
β’ (πΉ:π
βΆβ0 β πΉ:π
βontoβran πΉ) |
4 | 3 | ad2antlr 726 |
. . . . . 6
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
= β
) β πΉ:π
βontoβran πΉ) |
5 | | foeq2 6803 |
. . . . . . 7
β’ (π
= β
β (πΉ:π
βontoβran πΉ β πΉ:β
βontoβran πΉ)) |
6 | 5 | adantl 483 |
. . . . . 6
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
= β
) β (πΉ:π
βontoβran πΉ β πΉ:β
βontoβran πΉ)) |
7 | 4, 6 | mpbid 231 |
. . . . 5
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
= β
) β πΉ:β
βontoβran πΉ) |
8 | | fo00 6870 |
. . . . . 6
β’ (πΉ:β
βontoβran πΉ β (πΉ = β
β§ ran πΉ = β
)) |
9 | 8 | simplbi 499 |
. . . . 5
β’ (πΉ:β
βontoβran πΉ β πΉ = β
) |
10 | 7, 9 | syl 17 |
. . . 4
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
= β
) β πΉ = β
) |
11 | 10 | oveq2d 7425 |
. . 3
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
= β
) β (0 Ramsey
πΉ) = (0 Ramsey
β
)) |
12 | | 0nn0 12487 |
. . . . 5
β’ 0 β
β0 |
13 | | ram0 16955 |
. . . . 5
β’ (0 β
β0 β (0 Ramsey β
) = 0) |
14 | 12, 13 | ax-mp 5 |
. . . 4
β’ (0 Ramsey
β
) = 0 |
15 | 14, 12 | eqeltri 2830 |
. . 3
β’ (0 Ramsey
β
) β β0 |
16 | 11, 15 | eqeltrdi 2842 |
. 2
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
= β
) β (0 Ramsey
πΉ) β
β0) |
17 | | 0ram2 16954 |
. . . . 5
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β (0
Ramsey πΉ) = sup(ran πΉ, β, <
)) |
18 | | frn 6725 |
. . . . . . 7
β’ (πΉ:π
βΆβ0 β ran πΉ β
β0) |
19 | 18 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β ran
πΉ β
β0) |
20 | | nn0ssz 12581 |
. . . . . . . 8
β’
β0 β β€ |
21 | 19, 20 | sstrdi 3995 |
. . . . . . 7
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β ran
πΉ β
β€) |
22 | | fdm 6727 |
. . . . . . . . . 10
β’ (πΉ:π
βΆβ0 β dom πΉ = π
) |
23 | 22 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β dom
πΉ = π
) |
24 | | simp2 1138 |
. . . . . . . . 9
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β π
β β
) |
25 | 23, 24 | eqnetrd 3009 |
. . . . . . . 8
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β dom
πΉ β
β
) |
26 | | dm0rn0 5925 |
. . . . . . . . 9
β’ (dom
πΉ = β
β ran
πΉ =
β
) |
27 | 26 | necon3bii 2994 |
. . . . . . . 8
β’ (dom
πΉ β β
β ran
πΉ β
β
) |
28 | 25, 27 | sylib 217 |
. . . . . . 7
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β ran
πΉ β
β
) |
29 | | nn0ssre 12476 |
. . . . . . . . . 10
β’
β0 β β |
30 | 19, 29 | sstrdi 3995 |
. . . . . . . . 9
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β ran
πΉ β
β) |
31 | | simp1 1137 |
. . . . . . . . . 10
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β π
β Fin) |
32 | 3 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β πΉ:π
βontoβran πΉ) |
33 | | fofi 9338 |
. . . . . . . . . 10
β’ ((π
β Fin β§ πΉ:π
βontoβran πΉ) β ran πΉ β Fin) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . . . . . 9
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β ran
πΉ β
Fin) |
35 | | fimaxre 12158 |
. . . . . . . . 9
β’ ((ran
πΉ β β β§ ran
πΉ β Fin β§ ran
πΉ β β
) β
βπ₯ β ran πΉβπ¦ β ran πΉ π¦ β€ π₯) |
36 | 30, 34, 28, 35 | syl3anc 1372 |
. . . . . . . 8
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β
βπ₯ β ran πΉβπ¦ β ran πΉ π¦ β€ π₯) |
37 | | ssrexv 4052 |
. . . . . . . 8
β’ (ran
πΉ β β€ β
(βπ₯ β ran πΉβπ¦ β ran πΉ π¦ β€ π₯ β βπ₯ β β€ βπ¦ β ran πΉ π¦ β€ π₯)) |
38 | 21, 36, 37 | sylc 65 |
. . . . . . 7
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β
βπ₯ β β€
βπ¦ β ran πΉ π¦ β€ π₯) |
39 | | suprzcl2 12922 |
. . . . . . 7
β’ ((ran
πΉ β β€ β§ ran
πΉ β β
β§
βπ₯ β β€
βπ¦ β ran πΉ π¦ β€ π₯) β sup(ran πΉ, β, < ) β ran πΉ) |
40 | 21, 28, 38, 39 | syl3anc 1372 |
. . . . . 6
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β sup(ran
πΉ, β, < ) β
ran πΉ) |
41 | 19, 40 | sseldd 3984 |
. . . . 5
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β sup(ran
πΉ, β, < ) β
β0) |
42 | 17, 41 | eqeltrd 2834 |
. . . 4
β’ ((π
β Fin β§ π
β β
β§ πΉ:π
βΆβ0) β (0
Ramsey πΉ) β
β0) |
43 | 42 | 3expa 1119 |
. . 3
β’ (((π
β Fin β§ π
β β
) β§ πΉ:π
βΆβ0) β (0
Ramsey πΉ) β
β0) |
44 | 43 | an32s 651 |
. 2
β’ (((π
β Fin β§ πΉ:π
βΆβ0) β§ π
β β
) β (0 Ramsey
πΉ) β
β0) |
45 | 16, 44 | pm2.61dane 3030 |
1
β’ ((π
β Fin β§ πΉ:π
βΆβ0) β (0
Ramsey πΉ) β
β0) |