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

Definition df-ram 14367
 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.)
Assertion
Ref Expression
df-ram Ramsey
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-ram
StepHypRef Expression
1 cram 14365 . 2 Ramsey
2 vm . . 3
3 vr . . 3
4 cn0 10784 . . 3
5 cvv 3106 . . 3
6 vn . . . . . . . . 9
76cv 1373 . . . . . . . 8
8 vs . . . . . . . . . 10
98cv 1373 . . . . . . . . 9
10 chash 12360 . . . . . . . . 9
119, 10cfv 5579 . . . . . . . 8
12 cle 9618 . . . . . . . 8
137, 11, 12wbr 4440 . . . . . . 7
14 vc . . . . . . . . . . . . . 14
1514cv 1373 . . . . . . . . . . . . 13
163cv 1373 . . . . . . . . . . . . 13
1715, 16cfv 5579 . . . . . . . . . . . 12
18 vx . . . . . . . . . . . . . 14
1918cv 1373 . . . . . . . . . . . . 13
2019, 10cfv 5579 . . . . . . . . . . . 12
2117, 20, 12wbr 4440 . . . . . . . . . . 11
22 vy . . . . . . . . . . . . . . . 16
2322cv 1373 . . . . . . . . . . . . . . 15
2423, 10cfv 5579 . . . . . . . . . . . . . 14
252cv 1373 . . . . . . . . . . . . . 14
2624, 25wceq 1374 . . . . . . . . . . . . 13
27 vf . . . . . . . . . . . . . . . 16
2827cv 1373 . . . . . . . . . . . . . . 15
2923, 28cfv 5579 . . . . . . . . . . . . . 14
3029, 15wceq 1374 . . . . . . . . . . . . 13
3126, 30wi 4 . . . . . . . . . . . 12
3219cpw 4003 . . . . . . . . . . . 12
3331, 22, 32wral 2807 . . . . . . . . . . 11
3421, 33wa 369 . . . . . . . . . 10
359cpw 4003 . . . . . . . . . 10
3634, 18, 35wrex 2808 . . . . . . . . 9
3716cdm 4992 . . . . . . . . 9
3836, 14, 37wrex 2808 . . . . . . . 8
3926, 22, 35crab 2811 . . . . . . . . 9
40 cmap 7410 . . . . . . . . 9
4137, 39, 40co 6275 . . . . . . . 8
4238, 27, 41wral 2807 . . . . . . 7
4313, 42wi 4 . . . . . 6
4443, 8wal 1372 . . . . 5
4544, 6, 4crab 2811 . . . 4
46 cxr 9616 . . . 4
47 clt 9617 . . . . 5
4847ccnv 4991 . . . 4
4945, 46, 48csup 7889 . . 3
502, 3, 4, 5, 49cmpt2 6277 . 2
511, 50wceq 1374 1 Ramsey
 Colors of variables: wff setvar class This definition is referenced by:  ramval  14374
 Copyright terms: Public domain W3C validator