Metamath Proof Explorer

Theorem ramz

Description: The Ramsey number when F is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion ramz 
|- ( ( M e. NN0 /\ R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2 n0 
 |-  ( R =/= (/) <-> E. c c e. R )
3 simpll 
 |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> M e. NN )
4 simplr 
 |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> R e. V )
5 0nn0 
 |-  0 e. NN0
6 5 fconst6 
 |-  ( R X. { 0 } ) : R --> NN0
7 6 a1i 
 |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> ( R X. { 0 } ) : R --> NN0 )
8 simpr 
 |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> c e. R )
9 fvconst2g 
 |-  ( ( 0 e. NN0 /\ c e. R ) -> ( ( R X. { 0 } ) ` c ) = 0 )
10 5 8 9 sylancr 
 |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> ( ( R X. { 0 } ) ` c ) = 0 )
11 ramz2 
 |-  ( ( ( M e. NN /\ R e. V /\ ( R X. { 0 } ) : R --> NN0 ) /\ ( c e. R /\ ( ( R X. { 0 } ) ` c ) = 0 ) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )
12 3 4 7 8 10 11 syl32anc 
 |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )
13 12 ex 
 |-  ( ( M e. NN /\ R e. V ) -> ( c e. R -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
14 13 exlimdv 
 |-  ( ( M e. NN /\ R e. V ) -> ( E. c c e. R -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
15 2 14 syl5bi 
 |-  ( ( M e. NN /\ R e. V ) -> ( R =/= (/) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
16 15 expimpd 
 |-  ( M e. NN -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
17 simpl 
 |-  ( ( R e. V /\ R =/= (/) ) -> R e. V )
18 simpr 
 |-  ( ( R e. V /\ R =/= (/) ) -> R =/= (/) )
19 6 a1i 
 |-  ( ( R e. V /\ R =/= (/) ) -> ( R X. { 0 } ) : R --> NN0 )
20 0z 
 |-  0 e. ZZ
21 elsni 
 |-  ( y e. { 0 } -> y = 0 )
22 0le0 
 |-  0 <_ 0
23 21 22 eqbrtrdi 
 |-  ( y e. { 0 } -> y <_ 0 )
24 23 rgen 
 |-  A. y e. { 0 } y <_ 0
25 rnxp 
 |-  ( R =/= (/) -> ran ( R X. { 0 } ) = { 0 } )
26 25 adantl 
 |-  ( ( R e. V /\ R =/= (/) ) -> ran ( R X. { 0 } ) = { 0 } )
27 26 raleqdv 
 |-  ( ( R e. V /\ R =/= (/) ) -> ( A. y e. ran ( R X. { 0 } ) y <_ 0 <-> A. y e. { 0 } y <_ 0 ) )
28 24 27 mpbiri 
 |-  ( ( R e. V /\ R =/= (/) ) -> A. y e. ran ( R X. { 0 } ) y <_ 0 )
29 brralrspcev 
 |-  ( ( 0 e. ZZ /\ A. y e. ran ( R X. { 0 } ) y <_ 0 ) -> E. x e. ZZ A. y e. ran ( R X. { 0 } ) y <_ x )
30 20 28 29 sylancr 
 |-  ( ( R e. V /\ R =/= (/) ) -> E. x e. ZZ A. y e. ran ( R X. { 0 } ) y <_ x )
31 0ram 
 |-  ( ( ( R e. V /\ R =/= (/) /\ ( R X. { 0 } ) : R --> NN0 ) /\ E. x e. ZZ A. y e. ran ( R X. { 0 } ) y <_ x ) -> ( 0 Ramsey ( R X. { 0 } ) ) = sup ( ran ( R X. { 0 } ) , RR , < ) )
32 17 18 19 30 31 syl31anc 
 |-  ( ( R e. V /\ R =/= (/) ) -> ( 0 Ramsey ( R X. { 0 } ) ) = sup ( ran ( R X. { 0 } ) , RR , < ) )
33 26 supeq1d 
 |-  ( ( R e. V /\ R =/= (/) ) -> sup ( ran ( R X. { 0 } ) , RR , < ) = sup ( { 0 } , RR , < ) )
34 ltso 
 |-  < Or RR
35 0re 
 |-  0 e. RR
36 supsn 
 |-  ( ( < Or RR /\ 0 e. RR ) -> sup ( { 0 } , RR , < ) = 0 )
37 34 35 36 mp2an 
 |-  sup ( { 0 } , RR , < ) = 0
38 37 a1i 
 |-  ( ( R e. V /\ R =/= (/) ) -> sup ( { 0 } , RR , < ) = 0 )
39 32 33 38 3eqtrd 
 |-  ( ( R e. V /\ R =/= (/) ) -> ( 0 Ramsey ( R X. { 0 } ) ) = 0 )
40 oveq1 
 |-  ( M = 0 -> ( M Ramsey ( R X. { 0 } ) ) = ( 0 Ramsey ( R X. { 0 } ) ) )
41 40 eqeq1d 
 |-  ( M = 0 -> ( ( M Ramsey ( R X. { 0 } ) ) = 0 <-> ( 0 Ramsey ( R X. { 0 } ) ) = 0 ) )
42 39 41 syl5ibr 
 |-  ( M = 0 -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
43 16 42 jaoi 
 |-  ( ( M e. NN \/ M = 0 ) -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
44 1 43 sylbi 
 |-  ( M e. NN0 -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )
45 44 3impib 
 |-  ( ( M e. NN0 /\ R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )