Metamath Proof Explorer

Theorem ramub1

Description: Inductive step for Ramsey's theorem, in the form of an explicit upper bound. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m 
|- ( ph -> M e. NN )
ramub1.r 
|- ( ph -> R e. Fin )
ramub1.f 
|- ( ph -> F : R --> NN )
ramub1.g 
|- G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )
ramub1.1 
|- ( ph -> G : R --> NN0 )
ramub1.2 
|- ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )
Assertion ramub1 
|- ( ph -> ( M Ramsey F ) <_ ( ( ( M - 1 ) Ramsey G ) + 1 ) )

Proof

Step Hyp Ref Expression
1 ramub1.m 
 |-  ( ph -> M e. NN )
2 ramub1.r 
 |-  ( ph -> R e. Fin )
3 ramub1.f 
 |-  ( ph -> F : R --> NN )
4 ramub1.g 
 |-  G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )
5 ramub1.1 
 |-  ( ph -> G : R --> NN0 )
6 ramub1.2 
 |-  ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )
7 eqid 
 |-  ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
8 1 nnnn0d 
 |-  ( ph -> M e. NN0 )
9 nnssnn0 
 |-  NN C_ NN0
10 fss 
 |-  ( ( F : R --> NN /\ NN C_ NN0 ) -> F : R --> NN0 )
11 3 9 10 sylancl 
 |-  ( ph -> F : R --> NN0 )
12 peano2nn0 
 |-  ( ( ( M - 1 ) Ramsey G ) e. NN0 -> ( ( ( M - 1 ) Ramsey G ) + 1 ) e. NN0 )
13 6 12 syl 
 |-  ( ph -> ( ( ( M - 1 ) Ramsey G ) + 1 ) e. NN0 )
14 simprl 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )
15 6 adantr 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( ( M - 1 ) Ramsey G ) e. NN0 )
16 nn0p1nn 
 |-  ( ( ( M - 1 ) Ramsey G ) e. NN0 -> ( ( ( M - 1 ) Ramsey G ) + 1 ) e. NN )
17 15 16 syl 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( ( ( M - 1 ) Ramsey G ) + 1 ) e. NN )
18 14 17 eqeltrd 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( # ` s ) e. NN )
19 18 nnnn0d 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( # ` s ) e. NN0 )
20 hashclb 
 |-  ( s e. _V -> ( s e. Fin <-> ( # ` s ) e. NN0 ) )
21 20 elv 
 |-  ( s e. Fin <-> ( # ` s ) e. NN0 )
22 19 21 sylibr 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> s e. Fin )
23 hashnncl 
 |-  ( s e. Fin -> ( ( # ` s ) e. NN <-> s =/= (/) ) )
24 22 23 syl 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( ( # ` s ) e. NN <-> s =/= (/) ) )
25 18 24 mpbid 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> s =/= (/) )
26 n0 
 |-  ( s =/= (/) <-> E. w w e. s )
27 25 26 sylib 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> E. w w e. s )
28 1 adantr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> M e. NN )
29 2 adantr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> R e. Fin )
30 3 adantr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> F : R --> NN )
31 5 adantr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> G : R --> NN0 )
32 6 adantr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> ( ( M - 1 ) Ramsey G ) e. NN0 )
33 22 adantrr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> s e. Fin )
34 simprll 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )
35 simprlr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R )
36 simprr 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> w e. s )
37 uneq1 
 |-  ( v = u -> ( v u. { w } ) = ( u u. { w } ) )
38 37 fveq2d 
 |-  ( v = u -> ( f ` ( v u. { w } ) ) = ( f ` ( u u. { w } ) ) )
39 38 cbvmptv 
 |-  ( v e. ( ( s \ { w } ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) ( M - 1 ) ) |-> ( f ` ( v u. { w } ) ) ) = ( u e. ( ( s \ { w } ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) ( M - 1 ) ) |-> ( f ` ( u u. { w } ) ) )
40 28 29 30 4 31 32 7 33 34 35 36 39 ramub1lem2 
 |-  ( ( ph /\ ( ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) /\ w e. s ) ) -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) )
41 40 expr 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( w e. s -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) )
42 41 exlimdv 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( E. w w e. s -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) )
43 27 42 mpd 
 |-  ( ( ph /\ ( ( # ` s ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) )
44 7 8 2 11 13 43 ramub2 
 |-  ( ph -> ( M Ramsey F ) <_ ( ( ( M - 1 ) Ramsey G ) + 1 ) )