Step | Hyp | Ref
| Expression |
1 | | rami.c |
. 2
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) |
2 | | rami.m |
. 2
β’ (π β π β
β0) |
3 | | rami.r |
. 2
β’ (π β π
β π) |
4 | | rami.f |
. 2
β’ (π β πΉ:π
βΆβ0) |
5 | | ramub2.n |
. 2
β’ (π β π β
β0) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β π β
β0) |
7 | | hashfz1 14253 |
. . . . . . 7
β’ (π β β0
β (β―β(1...π)) = π) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β (β―β(1...π)) = π) |
9 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β π β€ (β―βπ‘)) |
10 | 8, 9 | eqbrtrd 5132 |
. . . . 5
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β (β―β(1...π)) β€ (β―βπ‘)) |
11 | | fzfid 13885 |
. . . . . 6
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β (1...π) β Fin) |
12 | | vex 3452 |
. . . . . 6
β’ π‘ β V |
13 | | hashdom 14286 |
. . . . . 6
β’
(((1...π) β Fin
β§ π‘ β V) β
((β―β(1...π))
β€ (β―βπ‘)
β (1...π) βΌ
π‘)) |
14 | 11, 12, 13 | sylancl 587 |
. . . . 5
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β ((β―β(1...π)) β€ (β―βπ‘) β (1...π) βΌ π‘)) |
15 | 10, 14 | mpbid 231 |
. . . 4
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β (1...π) βΌ π‘) |
16 | 12 | domen 8908 |
. . . 4
β’
((1...π) βΌ
π‘ β βπ ((1...π) β π β§ π β π‘)) |
17 | 15, 16 | sylib 217 |
. . 3
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β βπ ((1...π) β π β§ π β π‘)) |
18 | | simpll 766 |
. . . . 5
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β π) |
19 | | ensym 8950 |
. . . . . . . 8
β’
((1...π) β
π β π β (1...π)) |
20 | 19 | ad2antrl 727 |
. . . . . . 7
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β π β (1...π)) |
21 | | hasheni 14255 |
. . . . . . 7
β’ (π β (1...π) β (β―βπ ) = (β―β(1...π))) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (β―βπ ) = (β―β(1...π))) |
23 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β π β
β0) |
24 | 23, 7 | syl 17 |
. . . . . 6
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (β―β(1...π)) = π) |
25 | 22, 24 | eqtrd 2777 |
. . . . 5
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (β―βπ ) = π) |
26 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β π:(π‘πΆπ)βΆπ
) |
27 | | simprr 772 |
. . . . . . 7
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β π β π‘) |
28 | 2 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β π β
β0) |
29 | 1 | hashbcss 16883 |
. . . . . . 7
β’ ((π‘ β V β§ π β π‘ β§ π β β0) β (π πΆπ) β (π‘πΆπ)) |
30 | 12, 27, 28, 29 | mp3an2i 1467 |
. . . . . 6
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (π πΆπ) β (π‘πΆπ)) |
31 | 26, 30 | fssresd 6714 |
. . . . 5
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (π βΎ (π πΆπ)):(π πΆπ)βΆπ
) |
32 | | vex 3452 |
. . . . . . 7
β’ π β V |
33 | 32 | resex 5990 |
. . . . . 6
β’ (π βΎ (π πΆπ)) β V |
34 | | feq1 6654 |
. . . . . . . . 9
β’ (π = (π βΎ (π πΆπ)) β (π:(π πΆπ)βΆπ
β (π βΎ (π πΆπ)):(π πΆπ)βΆπ
)) |
35 | 34 | anbi2d 630 |
. . . . . . . 8
β’ (π = (π βΎ (π πΆπ)) β (((β―βπ ) = π β§ π:(π πΆπ)βΆπ
) β ((β―βπ ) = π β§ (π βΎ (π πΆπ)):(π πΆπ)βΆπ
))) |
36 | 35 | anbi2d 630 |
. . . . . . 7
β’ (π = (π βΎ (π πΆπ)) β ((π β§ ((β―βπ ) = π β§ π:(π πΆπ)βΆπ
)) β (π β§ ((β―βπ ) = π β§ (π βΎ (π πΆπ)):(π πΆπ)βΆπ
)))) |
37 | | cnveq 5834 |
. . . . . . . . . . . 12
β’ (π = (π βΎ (π πΆπ)) β β‘π = β‘(π βΎ (π πΆπ))) |
38 | 37 | imaeq1d 6017 |
. . . . . . . . . . 11
β’ (π = (π βΎ (π πΆπ)) β (β‘π β {π}) = (β‘(π βΎ (π πΆπ)) β {π})) |
39 | | cnvresima 6187 |
. . . . . . . . . . 11
β’ (β‘(π βΎ (π πΆπ)) β {π}) = ((β‘π β {π}) β© (π πΆπ)) |
40 | 38, 39 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π = (π βΎ (π πΆπ)) β (β‘π β {π}) = ((β‘π β {π}) β© (π πΆπ))) |
41 | 40 | sseq2d 3981 |
. . . . . . . . 9
β’ (π = (π βΎ (π πΆπ)) β ((π₯πΆπ) β (β‘π β {π}) β (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)))) |
42 | 41 | anbi2d 630 |
. . . . . . . 8
β’ (π = (π βΎ (π πΆπ)) β (((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π})) β ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ))))) |
43 | 42 | 2rexbidv 3214 |
. . . . . . 7
β’ (π = (π βΎ (π πΆπ)) β (βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π})) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ))))) |
44 | 36, 43 | imbi12d 345 |
. . . . . 6
β’ (π = (π βΎ (π πΆπ)) β (((π β§ ((β―βπ ) = π β§ π:(π πΆπ)βΆπ
)) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π}))) β ((π β§ ((β―βπ ) = π β§ (π βΎ (π πΆπ)):(π πΆπ)βΆπ
)) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)))))) |
45 | | ramub2.i |
. . . . . 6
β’ ((π β§ ((β―βπ ) = π β§ π:(π πΆπ)βΆπ
)) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π}))) |
46 | 33, 44, 45 | vtocl 3521 |
. . . . 5
β’ ((π β§ ((β―βπ ) = π β§ (π βΎ (π πΆπ)):(π πΆπ)βΆπ
)) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)))) |
47 | 18, 25, 31, 46 | syl12anc 836 |
. . . 4
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)))) |
48 | | sstr 3957 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π β π‘) β π₯ β π‘) |
49 | 48 | expcom 415 |
. . . . . . . . 9
β’ (π β π‘ β (π₯ β π β π₯ β π‘)) |
50 | 49 | ad2antll 728 |
. . . . . . . 8
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (π₯ β π β π₯ β π‘)) |
51 | | velpw 4570 |
. . . . . . . 8
β’ (π₯ β π« π β π₯ β π ) |
52 | | velpw 4570 |
. . . . . . . 8
β’ (π₯ β π« π‘ β π₯ β π‘) |
53 | 50, 51, 52 | 3imtr4g 296 |
. . . . . . 7
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (π₯ β π« π β π₯ β π« π‘)) |
54 | | id 22 |
. . . . . . . . . 10
β’ ((π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)) β (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ))) |
55 | | inss1 4193 |
. . . . . . . . . 10
β’ ((β‘π β {π}) β© (π πΆπ)) β (β‘π β {π}) |
56 | 54, 55 | sstrdi 3961 |
. . . . . . . . 9
β’ ((π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)) β (π₯πΆπ) β (β‘π β {π})) |
57 | 56 | a1i 11 |
. . . . . . . 8
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β ((π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)) β (π₯πΆπ) β (β‘π β {π}))) |
58 | 57 | anim2d 613 |
. . . . . . 7
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ))) β ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π})))) |
59 | 53, 58 | anim12d 610 |
. . . . . 6
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β ((π₯ β π« π β§ ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ)))) β (π₯ β π« π‘ β§ ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π}))))) |
60 | 59 | reximdv2 3162 |
. . . . 5
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ))) β βπ₯ β π« π‘((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π})))) |
61 | 60 | reximdv 3168 |
. . . 4
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β (βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β ((β‘π β {π}) β© (π πΆπ))) β βπ β π
βπ₯ β π« π‘((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π})))) |
62 | 47, 61 | mpd 15 |
. . 3
β’ (((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β§ ((1...π) β π β§ π β π‘)) β βπ β π
βπ₯ β π« π‘((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π}))) |
63 | 17, 62 | exlimddv 1939 |
. 2
β’ ((π β§ (π β€ (β―βπ‘) β§ π:(π‘πΆπ)βΆπ
)) β βπ β π
βπ₯ β π« π‘((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π}))) |
64 | 1, 2, 3, 4, 5, 63 | ramub 16892 |
1
β’ (π β (π Ramsey πΉ) β€ π) |