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

Definition df-ram 13048
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 13046 . 2  class Ramsey
2 vm . . 3  set  m
3 vr . . 3  set  r
4 cn0 9965 . . 3  class  NN0
5 cvv 2788 . . 3  class  _V
6 vn . . . . . . . . 9  set  n
76cv 1622 . . . . . . . 8  class  n
8 vs . . . . . . . . . 10  set  s
98cv 1622 . . . . . . . . 9  class  s
10 chash 11337 . . . . . . . . 9  class  #
119, 10cfv 5255 . . . . . . . 8  class  ( # `  s )
12 cle 8868 . . . . . . . 8  class  <_
137, 11, 12wbr 4023 . . . . . . 7  wff  n  <_ 
( # `  s )
14 vc . . . . . . . . . . . . . 14  set  c
1514cv 1622 . . . . . . . . . . . . 13  class  c
163cv 1622 . . . . . . . . . . . . 13  class  r
1715, 16cfv 5255 . . . . . . . . . . . 12  class  ( r `
 c )
18 vx . . . . . . . . . . . . . 14  set  x
1918cv 1622 . . . . . . . . . . . . 13  class  x
2019, 10cfv 5255 . . . . . . . . . . . 12  class  ( # `  x )
2117, 20, 12wbr 4023 . . . . . . . . . . 11  wff  ( r `
 c )  <_ 
( # `  x )
22 vy . . . . . . . . . . . . . . . 16  set  y
2322cv 1622 . . . . . . . . . . . . . . 15  class  y
2423, 10cfv 5255 . . . . . . . . . . . . . 14  class  ( # `  y )
252cv 1622 . . . . . . . . . . . . . 14  class  m
2624, 25wceq 1623 . . . . . . . . . . . . 13  wff  ( # `  y )  =  m
27 vf . . . . . . . . . . . . . . . 16  set  f
2827cv 1622 . . . . . . . . . . . . . . 15  class  f
2923, 28cfv 5255 . . . . . . . . . . . . . 14  class  ( f `
 y )
3029, 15wceq 1623 . . . . . . . . . . . . 13  wff  ( f `
 y )  =  c
3126, 30wi 4 . . . . . . . . . . . 12  wff  ( (
# `  y )  =  m  ->  ( f `
 y )  =  c )
3219cpw 3625 . . . . . . . . . . . 12  class  ~P x
3331, 22, 32wral 2543 . . . . . . . . . . 11  wff  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c )
3421, 33wa 358 . . . . . . . . . 10  wff  ( ( r `  c )  <_  ( # `  x
)  /\  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c ) )
359cpw 3625 . . . . . . . . . 10  class  ~P s
3634, 18, 35wrex 2544 . . . . . . . . 9  wff  E. x  e.  ~P  s ( ( r `  c )  <_  ( # `  x
)  /\  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c ) )
3716cdm 4689 . . . . . . . . 9  class  dom  r
3836, 14, 37wrex 2544 . . . . . . . 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 2547 . . . . . . . . 9  class  { y  e.  ~P s  |  ( # `  y
)  =  m }
40 cmap 6772 . . . . . . . . 9  class  ^m
4137, 39, 40co 5858 . . . . . . . 8  class  ( dom  r  ^m  { y  e.  ~P s  |  ( # `  y
)  =  m }
)
4238, 27, 41wral 2543 . . . . . . 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 1527 . . . . 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 2547 . . . 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 8866 . . . 4  class  RR*
47 clt 8867 . . . . 5  class  <
4847ccnv 4688 . . . 4  class  `'  <
4945, 46, 48csup 7193 . . 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 5860 . 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 1623 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 set class
This definition is referenced by:  ramval  13055
  Copyright terms: Public domain W3C validator