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

Definition df-ram 13371
 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 13369 . 2 Ramsey
2 vm . . 3
3 vr . . 3
4 cn0 10223 . . 3
5 cvv 2958 . . 3
6 vn . . . . . . . . 9
76cv 1652 . . . . . . . 8
8 vs . . . . . . . . . 10
98cv 1652 . . . . . . . . 9
10 chash 11620 . . . . . . . . 9
119, 10cfv 5456 . . . . . . . 8
12 cle 9123 . . . . . . . 8
137, 11, 12wbr 4214 . . . . . . 7
14 vc . . . . . . . . . . . . . 14
1514cv 1652 . . . . . . . . . . . . 13
163cv 1652 . . . . . . . . . . . . 13
1715, 16cfv 5456 . . . . . . . . . . . 12
18 vx . . . . . . . . . . . . . 14
1918cv 1652 . . . . . . . . . . . . 13
2019, 10cfv 5456 . . . . . . . . . . . 12
2117, 20, 12wbr 4214 . . . . . . . . . . 11
22 vy . . . . . . . . . . . . . . . 16
2322cv 1652 . . . . . . . . . . . . . . 15
2423, 10cfv 5456 . . . . . . . . . . . . . 14
252cv 1652 . . . . . . . . . . . . . 14
2624, 25wceq 1653 . . . . . . . . . . . . 13
27 vf . . . . . . . . . . . . . . . 16
2827cv 1652 . . . . . . . . . . . . . . 15
2923, 28cfv 5456 . . . . . . . . . . . . . 14
3029, 15wceq 1653 . . . . . . . . . . . . 13
3126, 30wi 4 . . . . . . . . . . . 12
3219cpw 3801 . . . . . . . . . . . 12
3331, 22, 32wral 2707 . . . . . . . . . . 11
3421, 33wa 360 . . . . . . . . . 10
359cpw 3801 . . . . . . . . . 10
3634, 18, 35wrex 2708 . . . . . . . . 9
3716cdm 4880 . . . . . . . . 9
3836, 14, 37wrex 2708 . . . . . . . 8
3926, 22, 35crab 2711 . . . . . . . . 9
40 cmap 7020 . . . . . . . . 9
4137, 39, 40co 6083 . . . . . . . 8
4238, 27, 41wral 2707 . . . . . . 7
4313, 42wi 4 . . . . . 6
4443, 8wal 1550 . . . . 5
4544, 6, 4crab 2711 . . . 4
46 cxr 9121 . . . 4
47 clt 9122 . . . . 5
4847ccnv 4879 . . . 4
4945, 46, 48csup 7447 . . 3
502, 3, 4, 5, 49cmpt2 6085 . 2
511, 50wceq 1653 1 Ramsey
 Colors of variables: wff set class This definition is referenced by:  ramval  13378
 Copyright terms: Public domain W3C validator