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* , < ) )