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

Definition df-ram 14912
 Description: Define the Ramsey number function. The input is a number for the size of the edges of the hypergraph, and a tuple from the finite color set to lower bounds for each color. The Ramsey number Ramsey is the smallest number such that for any set with Ramsey and any coloring of the set of -element subsets of (with color set ), there is a color and a subset such that and all the hyperedges of (that is, subsets of of size ) have color . (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
Assertion
Ref Expression
df-ram Ramsey inf
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-ram
StepHypRef Expression
1 cram 14909 . 2 Ramsey
2 vm . . 3
3 vr . . 3
4 cn0 10858 . . 3
5 cvv 3078 . . 3
6 vn . . . . . . . . 9
76cv 1436 . . . . . . . 8
8 vs . . . . . . . . . 10
98cv 1436 . . . . . . . . 9
10 chash 12501 . . . . . . . . 9
119, 10cfv 5592 . . . . . . . 8
12 cle 9665 . . . . . . . 8
137, 11, 12wbr 4417 . . . . . . 7
14 vc . . . . . . . . . . . . . 14
1514cv 1436 . . . . . . . . . . . . 13
163cv 1436 . . . . . . . . . . . . 13
1715, 16cfv 5592 . . . . . . . . . . . 12
18 vx . . . . . . . . . . . . . 14
1918cv 1436 . . . . . . . . . . . . 13
2019, 10cfv 5592 . . . . . . . . . . . 12
2117, 20, 12wbr 4417 . . . . . . . . . . 11
22 vy . . . . . . . . . . . . . . . 16
2322cv 1436 . . . . . . . . . . . . . . 15
2423, 10cfv 5592 . . . . . . . . . . . . . 14
252cv 1436 . . . . . . . . . . . . . 14
2624, 25wceq 1437 . . . . . . . . . . . . 13
27 vf . . . . . . . . . . . . . . . 16
2827cv 1436 . . . . . . . . . . . . . . 15
2923, 28cfv 5592 . . . . . . . . . . . . . 14
3029, 15wceq 1437 . . . . . . . . . . . . 13
3126, 30wi 4 . . . . . . . . . . . 12
3219cpw 3976 . . . . . . . . . . . 12
3331, 22, 32wral 2773 . . . . . . . . . . 11
3421, 33wa 370 . . . . . . . . . 10
359cpw 3976 . . . . . . . . . 10
3634, 18, 35wrex 2774 . . . . . . . . 9
3716cdm 4845 . . . . . . . . 9
3836, 14, 37wrex 2774 . . . . . . . 8
3926, 22, 35crab 2777 . . . . . . . . 9
40 cmap 7471 . . . . . . . . 9
4137, 39, 40co 6296 . . . . . . . 8
4238, 27, 41wral 2773 . . . . . . 7
4313, 42wi 4 . . . . . 6
4443, 8wal 1435 . . . . 5
4544, 6, 4crab 2777 . . . 4
46 cxr 9663 . . . 4
47 clt 9664 . . . 4
4845, 46, 47cinf 7952 . . 3 inf
492, 3, 4, 5, 48cmpt2 6298 . 2 inf
501, 49wceq 1437 1 Ramsey inf
 Colors of variables: wff setvar class This definition is referenced by:  ramval  14920
 Copyright terms: Public domain W3C validator