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

Definition df-ram 16038
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 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))}, ℝ*, < ))
Distinct variable group:   𝑓,𝑐,𝑥,𝑦,𝑚,𝑛,𝑟,𝑠

Detailed syntax breakdown of Definition df-ram
StepHypRef Expression
1 cram 16036 . 2 class Ramsey
2 vm . . 3 setvar 𝑚
3 vr . . 3 setvar 𝑟
4 cn0 11580 . . 3 class 0
5 cvv 3385 . . 3 class V
6 vn . . . . . . . . 9 setvar 𝑛
76cv 1652 . . . . . . . 8 class 𝑛
8 vs . . . . . . . . . 10 setvar 𝑠
98cv 1652 . . . . . . . . 9 class 𝑠
10 chash 13370 . . . . . . . . 9 class
119, 10cfv 6101 . . . . . . . 8 class (♯‘𝑠)
12 cle 10364 . . . . . . . 8 class
137, 11, 12wbr 4843 . . . . . . 7 wff 𝑛 ≤ (♯‘𝑠)
14 vc . . . . . . . . . . . . . 14 setvar 𝑐
1514cv 1652 . . . . . . . . . . . . 13 class 𝑐
163cv 1652 . . . . . . . . . . . . 13 class 𝑟
1715, 16cfv 6101 . . . . . . . . . . . 12 class (𝑟𝑐)
18 vx . . . . . . . . . . . . . 14 setvar 𝑥
1918cv 1652 . . . . . . . . . . . . 13 class 𝑥
2019, 10cfv 6101 . . . . . . . . . . . 12 class (♯‘𝑥)
2117, 20, 12wbr 4843 . . . . . . . . . . 11 wff (𝑟𝑐) ≤ (♯‘𝑥)
22 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
2322cv 1652 . . . . . . . . . . . . . . 15 class 𝑦
2423, 10cfv 6101 . . . . . . . . . . . . . 14 class (♯‘𝑦)
252cv 1652 . . . . . . . . . . . . . 14 class 𝑚
2624, 25wceq 1653 . . . . . . . . . . . . 13 wff (♯‘𝑦) = 𝑚
27 vf . . . . . . . . . . . . . . . 16 setvar 𝑓
2827cv 1652 . . . . . . . . . . . . . . 15 class 𝑓
2923, 28cfv 6101 . . . . . . . . . . . . . 14 class (𝑓𝑦)
3029, 15wceq 1653 . . . . . . . . . . . . 13 wff (𝑓𝑦) = 𝑐
3126, 30wi 4 . . . . . . . . . . . 12 wff ((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)
3219cpw 4349 . . . . . . . . . . . 12 class 𝒫 𝑥
3331, 22, 32wral 3089 . . . . . . . . . . 11 wff 𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)
3421, 33wa 385 . . . . . . . . . 10 wff ((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐))
359cpw 4349 . . . . . . . . . 10 class 𝒫 𝑠
3634, 18, 35wrex 3090 . . . . . . . . 9 wff 𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐))
3716cdm 5312 . . . . . . . . 9 class dom 𝑟
3836, 14, 37wrex 3090 . . . . . . . 8 wff 𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐))
3926, 22, 35crab 3093 . . . . . . . . 9 class {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚}
40 cmap 8095 . . . . . . . . 9 class 𝑚
4137, 39, 40co 6878 . . . . . . . 8 class (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})
4238, 27, 41wral 3089 . . . . . . 7 wff 𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐))
4313, 42wi 4 . . . . . 6 wff (𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))
4443, 8wal 1651 . . . . 5 wff 𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))
4544, 6, 4crab 3093 . . . 4 class {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))}
46 cxr 10362 . . . 4 class *
47 clt 10363 . . . 4 class <
4845, 46, 47cinf 8589 . . 3 class inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))}, ℝ*, < )
492, 3, 4, 5, 48cmpt2 6880 . 2 class (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))}, ℝ*, < ))
501, 49wceq 1653 1 wff Ramsey = (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟𝑚 {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟𝑥 ∈ 𝒫 𝑠((𝑟𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓𝑦) = 𝑐)))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  ramval  16045
  Copyright terms: Public domain W3C validator