Metamath Proof Explorer

Theorem ramlb

Description: Establish a lower bound on a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 ramlb.c 
 |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 ramlb.m 
 |-  ( ph -> M e. NN0 )
3 ramlb.r 
 |-  ( ph -> R e. V )
4 ramlb.f 
 |-  ( ph -> F : R --> NN0 )
5 ramlb.s 
 |-  ( ph -> N e. NN0 )
6 ramlb.g 
 |-  ( ph -> G : ( ( 1 ... N ) C M ) --> R )
7 ramlb.i 
 |-  ( ( ph /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( ( x C M ) C_ ( `' G " { c } ) -> ( # ` x ) < ( F ` c ) ) )
8 2 adantr 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> M e. NN0 )
9 3 adantr 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> R e. V )
10 4 adantr 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> F : R --> NN0 )
11 5 adantr 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> N e. NN0 )
12 simpr 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> ( M Ramsey F ) <_ N )
13 ramubcl 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( N e. NN0 /\ ( M Ramsey F ) <_ N ) ) -> ( M Ramsey F ) e. NN0 )
14 8 9 10 11 12 13 syl32anc 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> ( M Ramsey F ) e. NN0 )
15 fzfid 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> ( 1 ... N ) e. Fin )
16 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
17 5 16 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
18 17 breq2d 
 |-  ( ph -> ( ( M Ramsey F ) <_ ( # ` ( 1 ... N ) ) <-> ( M Ramsey F ) <_ N ) )
19 18 biimpar 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> ( M Ramsey F ) <_ ( # ` ( 1 ... N ) ) )
20 6 adantr 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> G : ( ( 1 ... N ) C M ) --> R )
21 1 8 9 10 14 15 19 20 rami 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> E. c e. R E. x e. ~P ( 1 ... N ) ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) )
22 elpwi 
 |-  ( x e. ~P ( 1 ... N ) -> x C_ ( 1 ... N ) )
23 7 adantlr 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( ( x C M ) C_ ( `' G " { c } ) -> ( # ` x ) < ( F ` c ) ) )
24 fzfid 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( 1 ... N ) e. Fin )
25 simprr 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> x C_ ( 1 ... N ) )
26 24 25 ssfid 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> x e. Fin )
27 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
28 26 27 syl 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( # ` x ) e. NN0 )
29 28 nn0red 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( # ` x ) e. RR )
30 simpl 
 |-  ( ( c e. R /\ x C_ ( 1 ... N ) ) -> c e. R )
31 ffvelrn 
 |-  ( ( F : R --> NN0 /\ c e. R ) -> ( F ` c ) e. NN0 )
32 10 30 31 syl2an 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( F ` c ) e. NN0 )
33 32 nn0red 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( F ` c ) e. RR )
34 29 33 ltnled 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( ( # ` x ) < ( F ` c ) <-> -. ( F ` c ) <_ ( # ` x ) ) )
35 23 34 sylibd 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( ( x C M ) C_ ( `' G " { c } ) -> -. ( F ` c ) <_ ( # ` x ) ) )
36 22 35 sylanr2 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x e. ~P ( 1 ... N ) ) ) -> ( ( x C M ) C_ ( `' G " { c } ) -> -. ( F ` c ) <_ ( # ` x ) ) )
37 36 con2d 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x e. ~P ( 1 ... N ) ) ) -> ( ( F ` c ) <_ ( # ` x ) -> -. ( x C M ) C_ ( `' G " { c } ) ) )
38 imnan 
 |-  ( ( ( F ` c ) <_ ( # ` x ) -> -. ( x C M ) C_ ( `' G " { c } ) ) <-> -. ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) )
39 37 38 sylib 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x e. ~P ( 1 ... N ) ) ) -> -. ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) )
40 39 pm2.21d 
 |-  ( ( ( ph /\ ( M Ramsey F ) <_ N ) /\ ( c e. R /\ x e. ~P ( 1 ... N ) ) ) -> ( ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) -> -. ( M Ramsey F ) <_ N ) )
41 40 rexlimdvva 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> ( E. c e. R E. x e. ~P ( 1 ... N ) ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) -> -. ( M Ramsey F ) <_ N ) )
42 21 41 mpd 
 |-  ( ( ph /\ ( M Ramsey F ) <_ N ) -> -. ( M Ramsey F ) <_ N )
43 42 pm2.01da 
 |-  ( ph -> -. ( M Ramsey F ) <_ N )
44 5 nn0red 
 |-  ( ph -> N e. RR )
45 44 rexrd 
 |-  ( ph -> N e. RR* )
46 ramxrcl 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. RR* )
47 2 3 4 46 syl3anc 
 |-  ( ph -> ( M Ramsey F ) e. RR* )
48 xrltnle 
 |-  ( ( N e. RR* /\ ( M Ramsey F ) e. RR* ) -> ( N < ( M Ramsey F ) <-> -. ( M Ramsey F ) <_ N ) )
49 45 47 48 syl2anc 
 |-  ( ph -> ( N < ( M Ramsey F ) <-> -. ( M Ramsey F ) <_ N ) )
50 43 49 mpbird 
 |-  ( ph -> N < ( M Ramsey F ) )