Definition df-ram 17026

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 dom 𝑅), there is a color 𝑐 ∈ dom 𝑅 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 = (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ))

Distinct variable group:   𝑓,𝑐,𝑥,𝑦,𝑚,𝑛,𝑟,𝑠

Detailed syntax breakdown of Definition df-ram

Step	Hyp	Ref	Expression
1		cram 17024	. 2 class Ramsey
2		vm	. . 3 setvar 𝑚
3		vr	. . 3 setvar 𝑟
4		cn0 12506	. . 3 class ℕ0
5		cvv 3464	. . 3 class V
6		vn	. . . . . . . . 9 setvar 𝑛
7	6	cv 1539	. . . . . . . 8 class 𝑛
8		vs	. . . . . . . . . 10 setvar 𝑠
9	8	cv 1539	. . . . . . . . 9 class 𝑠
10		chash 14353	. . . . . . . . 9 class ♯
11	9, 10	cfv 6536	. . . . . . . 8 class (♯‘𝑠)
12		cle 11275	. . . . . . . 8 class ≤
13	7, 11, 12	wbr 5124	. . . . . . 7 wff 𝑛 ≤ (♯‘𝑠)
14		vc	. . . . . . . . . . . . . 14 setvar 𝑐
15	14	cv 1539	. . . . . . . . . . . . 13 class 𝑐
16	3	cv 1539	. . . . . . . . . . . . 13 class 𝑟
17	15, 16	cfv 6536	. . . . . . . . . . . 12 class (𝑟‘𝑐)
18		vx	. . . . . . . . . . . . . 14 setvar 𝑥
19	18	cv 1539	. . . . . . . . . . . . 13 class 𝑥
20	19, 10	cfv 6536	. . . . . . . . . . . 12 class (♯‘𝑥)
21	17, 20, 12	wbr 5124	. . . . . . . . . . 11 wff (𝑟‘𝑐) ≤ (♯‘𝑥)
22		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
23	22	cv 1539	. . . . . . . . . . . . . . 15 class 𝑦
24	23, 10	cfv 6536	. . . . . . . . . . . . . 14 class (♯‘𝑦)
25	2	cv 1539	. . . . . . . . . . . . . 14 class 𝑚
26	24, 25	wceq 1540	. . . . . . . . . . . . 13 wff (♯‘𝑦) = 𝑚
27		vf	. . . . . . . . . . . . . . . 16 setvar 𝑓
28	27	cv 1539	. . . . . . . . . . . . . . 15 class 𝑓
29	23, 28	cfv 6536	. . . . . . . . . . . . . 14 class (𝑓‘𝑦)
30	29, 15	wceq 1540	. . . . . . . . . . . . 13 wff (𝑓‘𝑦) = 𝑐
31	26, 30	wi 4	. . . . . . . . . . . 12 wff ((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)
32	19	cpw 4580	. . . . . . . . . . . 12 class 𝒫 𝑥
33	31, 22, 32	wral 3052	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)
34	21, 33	wa 395	. . . . . . . . . 10 wff ((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))
35	9	cpw 4580	. . . . . . . . . 10 class 𝒫 𝑠
36	34, 18, 35	wrex 3061	. . . . . . . . 9 wff ∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))
37	16	cdm 5659	. . . . . . . . 9 class dom 𝑟
38	36, 14, 37	wrex 3061	. . . . . . . 8 wff ∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))
39	26, 22, 35	crab 3420	. . . . . . . . 9 class {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚}
40		cmap 8845	. . . . . . . . 9 class ↑m
41	37, 39, 40	co 7410	. . . . . . . 8 class (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})
42	38, 27, 41	wral 3052	. . . . . . 7 wff ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))
43	13, 42	wi 4	. . . . . 6 wff (𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))
44	43, 8	wal 1538	. . . . 5 wff ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))
45	44, 6, 4	crab 3420	. . . 4 class {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}
46		cxr 11273	. . . 4 class ℝ*
47		clt 11274	. . . 4 class <
48	45, 46, 47	cinf 9458	. . 3 class inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < )
49	2, 3, 4, 5, 48	cmpo 7412	. 2 class (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ))
50	1, 49	wceq 1540	1 wff Ramsey = (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ))

This definition is referenced by:  ramval  17033