# 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 )`