Metamath Proof Explorer

Theorem ramub2

Description: It is sufficient to check the Ramsey property on finite sets of size equal to the upper bound. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses rami.c 
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
rami.m 
|- ( ph -> M e. NN0 )
rami.r 
|- ( ph -> R e. V )
rami.f 
|- ( ph -> F : R --> NN0 )
ramub2.n 
|- ( ph -> N e. NN0 )
ramub2.i 
|- ( ( ph /\ ( ( # ` s ) = N /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )
Assertion ramub2 
|- ( ph -> ( M Ramsey F ) <_ N )

Proof

Step Hyp Ref Expression
1 rami.c 
 |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 rami.m 
 |-  ( ph -> M e. NN0 )
3 rami.r 
 |-  ( ph -> R e. V )
4 rami.f 
 |-  ( ph -> F : R --> NN0 )
5 ramub2.n 
 |-  ( ph -> N e. NN0 )
6 ramub2.i 
 |-  ( ( ph /\ ( ( # ` s ) = N /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )
7 5 adantr 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> N e. NN0 )
8 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
9 7 8 syl 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> ( # ` ( 1 ... N ) ) = N )
10 simprl 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> N <_ ( # ` t ) )
11 9 10 eqbrtrd 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> ( # ` ( 1 ... N ) ) <_ ( # ` t ) )
12 fzfid 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> ( 1 ... N ) e. Fin )
13 vex 
 |-  t e. _V
14 hashdom 
 |-  ( ( ( 1 ... N ) e. Fin /\ t e. _V ) -> ( ( # ` ( 1 ... N ) ) <_ ( # ` t ) <-> ( 1 ... N ) ~<_ t ) )
15 12 13 14 sylancl 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> ( ( # ` ( 1 ... N ) ) <_ ( # ` t ) <-> ( 1 ... N ) ~<_ t ) )
16 11 15 mpbid 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> ( 1 ... N ) ~<_ t )
17 13 domen 
 |-  ( ( 1 ... N ) ~<_ t <-> E. s ( ( 1 ... N ) ~~ s /\ s C_ t ) )
18 16 17 sylib 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> E. s ( ( 1 ... N ) ~~ s /\ s C_ t ) )
19 simpll 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ph )
20 ensym 
 |-  ( ( 1 ... N ) ~~ s -> s ~~ ( 1 ... N ) )
21 20 ad2antrl 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> s ~~ ( 1 ... N ) )
22 hasheni 
 |-  ( s ~~ ( 1 ... N ) -> ( # ` s ) = ( # ` ( 1 ... N ) ) )
23 21 22 syl 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( # ` s ) = ( # ` ( 1 ... N ) ) )
24 5 ad2antrr 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> N e. NN0 )
25 24 8 syl 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( # ` ( 1 ... N ) ) = N )
26 23 25 eqtrd 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( # ` s ) = N )
27 simplrr 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> g : ( t C M ) --> R )
28 simprr 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> s C_ t )
29 2 ad2antrr 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> M e. NN0 )
30 1 hashbcss 
 |-  ( ( t e. _V /\ s C_ t /\ M e. NN0 ) -> ( s C M ) C_ ( t C M ) )
31 13 28 29 30 mp3an2i 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( s C M ) C_ ( t C M ) )
32 27 31 fssresd 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( g |` ( s C M ) ) : ( s C M ) --> R )
33 vex 
 |-  g e. _V
34 33 resex 
 |-  ( g |` ( s C M ) ) e. _V
35 feq1 
 |-  ( f = ( g |` ( s C M ) ) -> ( f : ( s C M ) --> R <-> ( g |` ( s C M ) ) : ( s C M ) --> R ) )
36 35 anbi2d 
 |-  ( f = ( g |` ( s C M ) ) -> ( ( ( # ` s ) = N /\ f : ( s C M ) --> R ) <-> ( ( # ` s ) = N /\ ( g |` ( s C M ) ) : ( s C M ) --> R ) ) )
37 36 anbi2d 
 |-  ( f = ( g |` ( s C M ) ) -> ( ( ph /\ ( ( # ` s ) = N /\ f : ( s C M ) --> R ) ) <-> ( ph /\ ( ( # ` s ) = N /\ ( g |` ( s C M ) ) : ( s C M ) --> R ) ) ) )
38 cnveq 
 |-  ( f = ( g |` ( s C M ) ) -> `' f = `' ( g |` ( s C M ) ) )
39 38 imaeq1d 
 |-  ( f = ( g |` ( s C M ) ) -> ( `' f " { c } ) = ( `' ( g |` ( s C M ) ) " { c } ) )
40 cnvresima 
 |-  ( `' ( g |` ( s C M ) ) " { c } ) = ( ( `' g " { c } ) i^i ( s C M ) )
41 39 40 eqtrdi 
 |-  ( f = ( g |` ( s C M ) ) -> ( `' f " { c } ) = ( ( `' g " { c } ) i^i ( s C M ) ) )
42 41 sseq2d 
 |-  ( f = ( g |` ( s C M ) ) -> ( ( x C M ) C_ ( `' f " { c } ) <-> ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) )
43 42 anbi2d 
 |-  ( f = ( g |` ( s C M ) ) -> ( ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) <-> ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) ) )
44 43 2rexbidv 
 |-  ( f = ( g |` ( s C M ) ) -> ( E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) <-> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) ) )
45 37 44 imbi12d 
 |-  ( f = ( g |` ( s C M ) ) -> ( ( ( ph /\ ( ( # ` s ) = N /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) <-> ( ( ph /\ ( ( # ` s ) = N /\ ( g |` ( s C M ) ) : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) ) ) )
46 34 45 6 vtocl 
 |-  ( ( ph /\ ( ( # ` s ) = N /\ ( g |` ( s C M ) ) : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) )
47 19 26 32 46 syl12anc 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) )
48 sstr 
 |-  ( ( x C_ s /\ s C_ t ) -> x C_ t )
49 48 expcom 
 |-  ( s C_ t -> ( x C_ s -> x C_ t ) )
50 49 ad2antll 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( x C_ s -> x C_ t ) )
51 velpw 
 |-  ( x e. ~P s <-> x C_ s )
52 velpw 
 |-  ( x e. ~P t <-> x C_ t )
53 50 51 52 3imtr4g 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( x e. ~P s -> x e. ~P t ) )
54 id 
 |-  ( ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) -> ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) )
55 inss1 
 |-  ( ( `' g " { c } ) i^i ( s C M ) ) C_ ( `' g " { c } )
56 54 55 sstrdi 
 |-  ( ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) -> ( x C M ) C_ ( `' g " { c } ) )
57 56 a1i 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) -> ( x C M ) C_ ( `' g " { c } ) ) )
58 57 anim2d 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) -> ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' g " { c } ) ) ) )
59 53 58 anim12d 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( ( x e. ~P s /\ ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) ) -> ( x e. ~P t /\ ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' g " { c } ) ) ) ) )
60 59 reximdv2 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) -> E. x e. ~P t ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' g " { c } ) ) ) )
61 60 reximdv 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> ( E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( ( `' g " { c } ) i^i ( s C M ) ) ) -> E. c e. R E. x e. ~P t ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' g " { c } ) ) ) )
62 47 61 mpd 
 |-  ( ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) /\ ( ( 1 ... N ) ~~ s /\ s C_ t ) ) -> E. c e. R E. x e. ~P t ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' g " { c } ) ) )
63 18 62 exlimddv 
 |-  ( ( ph /\ ( N <_ ( # ` t ) /\ g : ( t C M ) --> R ) ) -> E. c e. R E. x e. ~P t ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' g " { c } ) ) )
64 1 2 3 4 5 63 ramub 
 |-  ( ph -> ( M Ramsey F ) <_ N )