# Metamath Proof Explorer

## Definition df-ram

Description: Define the Ramsey number function. The input is a number m for the size of the edges of the hypergraph, and a tuple r from the finite color set to lower bounds for each color. The Ramsey number ( M Ramsey R ) is the smallest number such that for any set S with ( M Ramsey R ) <_ # S and any coloring F of the set of M -element subsets of S (with color set dom R ), there is a color c e. dom R and a subset x C_ S such that R ( c ) <_ # x and all the hyperedges of x (that is, subsets of x of size M ) have color c . (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Assertion df-ram
`|- Ramsey = ( m e. NN0 , r e. _V |-> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) )`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cram
` |-  Ramsey`
1 vm
` |-  m`
2 cn0
` |-  NN0`
3 vr
` |-  r`
4 cvv
` |-  _V`
5 vn
` |-  n`
6 vs
` |-  s`
7 5 cv
` |-  n`
8 cle
` |-  <_`
9 chash
` |-  #`
10 6 cv
` |-  s`
11 10 9 cfv
` |-  ( # ` s )`
12 7 11 8 wbr
` |-  n <_ ( # ` s )`
13 vf
` |-  f`
14 3 cv
` |-  r`
15 14 cdm
` |-  dom r`
16 cmap
` |-  ^m`
17 vy
` |-  y`
18 10 cpw
` |-  ~P s`
19 17 cv
` |-  y`
20 19 9 cfv
` |-  ( # ` y )`
21 1 cv
` |-  m`
22 20 21 wceq
` |-  ( # ` y ) = m`
23 22 17 18 crab
` |-  { y e. ~P s | ( # ` y ) = m }`
24 15 23 16 co
` |-  ( dom r ^m { y e. ~P s | ( # ` y ) = m } )`
25 vc
` |-  c`
26 vx
` |-  x`
27 25 cv
` |-  c`
28 27 14 cfv
` |-  ( r ` c )`
29 26 cv
` |-  x`
30 29 9 cfv
` |-  ( # ` x )`
31 28 30 8 wbr
` |-  ( r ` c ) <_ ( # ` x )`
32 29 cpw
` |-  ~P x`
33 13 cv
` |-  f`
34 19 33 cfv
` |-  ( f ` y )`
35 34 27 wceq
` |-  ( f ` y ) = c`
36 22 35 wi
` |-  ( ( # ` y ) = m -> ( f ` y ) = c )`
37 36 17 32 wral
` |-  A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c )`
38 31 37 wa
` |-  ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) )`
39 38 26 18 wrex
` |-  E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) )`
40 39 25 15 wrex
` |-  E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) )`
41 40 13 24 wral
` |-  A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) )`
42 12 41 wi
` |-  ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) )`
43 42 6 wal
` |-  A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) )`
44 43 5 2 crab
` |-  { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) }`
45 cxr
` |-  RR*`
46 clt
` |-  <`
47 44 45 46 cinf
` |-  inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < )`
48 1 3 2 4 47 cmpo
` |-  ( m e. NN0 , r e. _V |-> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) )`
49 0 48 wceq
` |-  Ramsey = ( m e. NN0 , r e. _V |-> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) )`