MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ram Structured version   Unicode version

Definition df-ram 14164
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.)
Assertion
Ref Expression
df-ram  |- Ramsey  =  ( m  e.  NN0 , 
r  e.  _V  |->  sup ( { 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* ,  `'  <  ) )
Distinct variable group:    f, c, x, y, m, n, r, s

Detailed syntax breakdown of Definition df-ram
StepHypRef Expression
1 cram 14162 . 2  class Ramsey
2 vm . . 3  setvar  m
3 vr . . 3  setvar  r
4 cn0 10680 . . 3  class  NN0
5 cvv 3068 . . 3  class  _V
6 vn . . . . . . . . 9  setvar  n
76cv 1369 . . . . . . . 8  class  n
8 vs . . . . . . . . . 10  setvar  s
98cv 1369 . . . . . . . . 9  class  s
10 chash 12204 . . . . . . . . 9  class  #
119, 10cfv 5516 . . . . . . . 8  class  ( # `  s )
12 cle 9520 . . . . . . . 8  class  <_
137, 11, 12wbr 4390 . . . . . . 7  wff  n  <_ 
( # `  s )
14 vc . . . . . . . . . . . . . 14  setvar  c
1514cv 1369 . . . . . . . . . . . . 13  class  c
163cv 1369 . . . . . . . . . . . . 13  class  r
1715, 16cfv 5516 . . . . . . . . . . . 12  class  ( r `
 c )
18 vx . . . . . . . . . . . . . 14  setvar  x
1918cv 1369 . . . . . . . . . . . . 13  class  x
2019, 10cfv 5516 . . . . . . . . . . . 12  class  ( # `  x )
2117, 20, 12wbr 4390 . . . . . . . . . . 11  wff  ( r `
 c )  <_ 
( # `  x )
22 vy . . . . . . . . . . . . . . . 16  setvar  y
2322cv 1369 . . . . . . . . . . . . . . 15  class  y
2423, 10cfv 5516 . . . . . . . . . . . . . 14  class  ( # `  y )
252cv 1369 . . . . . . . . . . . . . 14  class  m
2624, 25wceq 1370 . . . . . . . . . . . . 13  wff  ( # `  y )  =  m
27 vf . . . . . . . . . . . . . . . 16  setvar  f
2827cv 1369 . . . . . . . . . . . . . . 15  class  f
2923, 28cfv 5516 . . . . . . . . . . . . . 14  class  ( f `
 y )
3029, 15wceq 1370 . . . . . . . . . . . . 13  wff  ( f `
 y )  =  c
3126, 30wi 4 . . . . . . . . . . . 12  wff  ( (
# `  y )  =  m  ->  ( f `
 y )  =  c )
3219cpw 3958 . . . . . . . . . . . 12  class  ~P x
3331, 22, 32wral 2795 . . . . . . . . . . 11  wff  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c )
3421, 33wa 369 . . . . . . . . . 10  wff  ( ( r `  c )  <_  ( # `  x
)  /\  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c ) )
359cpw 3958 . . . . . . . . . 10  class  ~P s
3634, 18, 35wrex 2796 . . . . . . . . 9  wff  E. x  e.  ~P  s ( ( r `  c )  <_  ( # `  x
)  /\  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c ) )
3716cdm 4938 . . . . . . . . 9  class  dom  r
3836, 14, 37wrex 2796 . . . . . . . 8  wff  E. c  e.  dom  r E. x  e.  ~P  s ( ( r `  c )  <_  ( # `  x
)  /\  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c ) )
3926, 22, 35crab 2799 . . . . . . . . 9  class  { y  e.  ~P s  |  ( # `  y
)  =  m }
40 cmap 7314 . . . . . . . . 9  class  ^m
4137, 39, 40co 6190 . . . . . . . 8  class  ( dom  r  ^m  { y  e.  ~P s  |  ( # `  y
)  =  m }
)
4238, 27, 41wral 2795 . . . . . . 7  wff  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 ) )
4313, 42wi 4 . . . . . 6  wff  ( 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 ) ) )
4443, 8wal 1368 . . . . 5  wff  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 ) ) )
4544, 6, 4crab 2799 . . . 4  class  { 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 ) ) ) }
46 cxr 9518 . . . 4  class  RR*
47 clt 9519 . . . . 5  class  <
4847ccnv 4937 . . . 4  class  `'  <
4945, 46, 48csup 7791 . . 3  class  sup ( { 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* ,  `'  <  )
502, 3, 4, 5, 49cmpt2 6192 . 2  class  ( m  e.  NN0 ,  r  e.  _V  |->  sup ( { 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* ,  `'  <  ) )
511, 50wceq 1370 1  wff Ramsey  =  ( m  e.  NN0 , 
r  e.  _V  |->  sup ( { 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* ,  `'  <  ) )
Colors of variables: wff setvar class
This definition is referenced by:  ramval  14171
  Copyright terms: Public domain W3C validator