Definition df-ram 15705

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.)

Assertion

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

Distinct variable group:   f, c, x, y, m, n, r, s

Detailed syntax breakdown of Definition df-ram

Step	Hyp	Ref	Expression
1		cram 15703	. 2 class Ramsey
2		vm	. . 3 setvar m
3		vr	. . 3 setvar r
4		cn0 11292	. . 3 class NN0
5		cvv 3200	. . 3 class _V
6		vn	. . . . . . . . 9 setvar n
7	6	cv 1482	. . . . . . . 8 class n
8		vs	. . . . . . . . . 10 setvar s
9	8	cv 1482	. . . . . . . . 9 class s
10		chash 13117	. . . . . . . . 9 class #
11	9, 10	cfv 5888	. . . . . . . 8 class ( # ` s )
12		cle 10075	. . . . . . . 8 class <_
13	7, 11, 12	wbr 4653	. . . . . . 7 wff n <_ ( # ` s )
14		vc	. . . . . . . . . . . . . 14 setvar c
15	14	cv 1482	. . . . . . . . . . . . 13 class c
16	3	cv 1482	. . . . . . . . . . . . 13 class r
17	15, 16	cfv 5888	. . . . . . . . . . . 12 class ( r ` c )
18		vx	. . . . . . . . . . . . . 14 setvar x
19	18	cv 1482	. . . . . . . . . . . . 13 class x
20	19, 10	cfv 5888	. . . . . . . . . . . 12 class ( # ` x )
21	17, 20, 12	wbr 4653	. . . . . . . . . . 11 wff ( r ` c ) <_ ( # ` x )
22		vy	. . . . . . . . . . . . . . . 16 setvar y
23	22	cv 1482	. . . . . . . . . . . . . . 15 class y
24	23, 10	cfv 5888	. . . . . . . . . . . . . 14 class ( # ` y )
25	2	cv 1482	. . . . . . . . . . . . . 14 class m
26	24, 25	wceq 1483	. . . . . . . . . . . . 13 wff ( # ` y ) = m
27		vf	. . . . . . . . . . . . . . . 16 setvar f
28	27	cv 1482	. . . . . . . . . . . . . . 15 class f
29	23, 28	cfv 5888	. . . . . . . . . . . . . 14 class ( f ` y )
30	29, 15	wceq 1483	. . . . . . . . . . . . 13 wff ( f ` y ) = c
31	26, 30	wi 4	. . . . . . . . . . . 12 wff ( ( # ` y ) = m -> ( f ` y ) = c )
32	19	cpw 4158	. . . . . . . . . . . 12 class ~P x
33	31, 22, 32	wral 2912	. . . . . . . . . . 11 wff A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c )
34	21, 33	wa 384	. . . . . . . . . 10 wff ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) )
35	9	cpw 4158	. . . . . . . . . 10 class ~P s
36	34, 18, 35	wrex 2913	. . . . . . . . 9 wff E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) )
37	16	cdm 5114	. . . . . . . . 9 class dom r
38	36, 14, 37	wrex 2913	. . . . . . . 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 ) )
39	26, 22, 35	crab 2916	. . . . . . . . 9 class { y e. ~P s | ( # ` y ) = m }
40		cmap 7857	. . . . . . . . 9 class ^m
41	37, 39, 40	co 6650	. . . . . . . 8 class ( dom r ^m { y e. ~P s | ( # ` y ) = m } )
42	38, 27, 41	wral 2912	. . . . . . 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 ) )
43	13, 42	wi 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 ) ) )
44	43, 8	wal 1481	. . . . 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 ) ) )
45	44, 6, 4	crab 2916	. . . 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 10073	. . . 4 class RR*
47		clt 10074	. . . 4 class <
48	45, 46, 47	cinf 8347	. . 3 class 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	2, 3, 4, 5, 48	cmpt2 6652	. 2 class ( 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* , < ) )
50	1, 49	wceq 1483	1 wff 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* , < ) )

This definition is referenced by:  ramval  15712