Metamath Proof Explorer

Theorem ramz2

Description: The Ramsey number when F has value zero for some color C . (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion ramz2 
|- ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> ( M Ramsey F ) = 0 )

Proof

Step Hyp Ref Expression
1 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 } )
2 simpl1 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> M e. NN )
3 2 nnnn0d 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> M e. NN0 )
4 simpl2 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> R e. V )
5 simpl3 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> F : R --> NN0 )
6 0nn0 
 |-  0 e. NN0
7 6 a1i 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> 0 e. NN0 )
8 simplrl 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> C e. R )
9 0elpw 
 |-  (/) e. ~P s
10 9 a1i 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> (/) e. ~P s )
11 simplrr 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( F ` C ) = 0 )
12 0le0 
 |-  0 <_ 0
13 11 12 eqbrtrdi 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( F ` C ) <_ 0 )
14 simpll1 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> M e. NN )
15 1 0hashbc 
 |-  ( M e. NN -> ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) )
16 14 15 syl 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) )
17 0ss 
 |-  (/) C_ ( `' f " { C } )
18 16 17 eqsstrdi 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) )
19 fveq2 
 |-  ( c = C -> ( F ` c ) = ( F ` C ) )
20 19 breq1d 
 |-  ( c = C -> ( ( F ` c ) <_ ( # ` x ) <-> ( F ` C ) <_ ( # ` x ) ) )
21 sneq 
 |-  ( c = C -> { c } = { C } )
22 21 imaeq2d 
 |-  ( c = C -> ( `' f " { c } ) = ( `' f " { C } ) )
23 22 sseq2d 
 |-  ( c = C -> ( ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) <-> ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) ) )
24 20 23 anbi12d 
 |-  ( c = C -> ( ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) <-> ( ( F ` C ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) ) ) )
25 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
26 hash0 
 |-  ( # ` (/) ) = 0
27 25 26 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
28 27 breq2d 
 |-  ( x = (/) -> ( ( F ` C ) <_ ( # ` x ) <-> ( F ` C ) <_ 0 ) )
29 oveq1 
 |-  ( x = (/) -> ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) )
30 29 sseq1d 
 |-  ( x = (/) -> ( ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) <-> ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) ) )
31 28 30 anbi12d 
 |-  ( x = (/) -> ( ( ( F ` C ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) ) <-> ( ( F ` C ) <_ 0 /\ ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) ) ) )
32 24 31 rspc2ev 
 |-  ( ( C e. R /\ (/) e. ~P s /\ ( ( F ` C ) <_ 0 /\ ( (/) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { C } ) ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) )
33 8 10 13 18 32 syl112anc 
 |-  ( ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) /\ ( 0 <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) )
34 1 3 4 5 7 33 ramub 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> ( M Ramsey F ) <_ 0 )
35 ramubcl 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( 0 e. NN0 /\ ( M Ramsey F ) <_ 0 ) ) -> ( M Ramsey F ) e. NN0 )
36 3 4 5 7 34 35 syl32anc 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> ( M Ramsey F ) e. NN0 )
37 nn0le0eq0 
 |-  ( ( M Ramsey F ) e. NN0 -> ( ( M Ramsey F ) <_ 0 <-> ( M Ramsey F ) = 0 ) )
38 36 37 syl 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> ( ( M Ramsey F ) <_ 0 <-> ( M Ramsey F ) = 0 ) )
39 34 38 mpbid 
 |-  ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> ( M Ramsey F ) = 0 )