# 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 } ) ) )
|-  ( ( 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 ) )
|-  ( ( ( 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 ) ) )
|-  ( ( ( 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 )
|-  ( ( ( 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 ) )
|-  ( ( ( 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 )