Metamath Proof Explorer

Definition df-ram

Description: Define the Ramsey number function. The input is a number m for the size of the edges of the hypergraph, and a tuple r from the finite color set to lower bounds for each color. The Ramsey number ( M Ramsey R ) is the smallest number such that for any set S with ( M Ramsey R ) <_ # S and any coloring F of the set of M -element subsets of S (with color set dom R ), there is a color c e. dom R and a subset x C_ S such that R ( c ) <_ # x and all the hyperedges of x (that is, subsets of x of size M ) have color c . (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Assertion df-ram ⊢ Ramsey = m ∈ ℕ 0 , r ∈ V ⟼ inf n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cram class Ramsey
1 vm setvar m
2 cn0 class ℕ 0
3 vr setvar r
4 cvv class V
5 vn setvar n
6 vs setvar s
7 5 cv setvar n
8 cle class ≤
9 chash class .
10 6 cv setvar s
11 10 9 cfv class s
12 7 11 8 wbr wff n ≤ s
13 vf setvar f
14 3 cv setvar r
15 14 cdm class dom ⁡ r
16 cmap class ↑ 𝑚
17 vy setvar y
18 10 cpw class 𝒫 s
19 17 cv setvar y
20 19 9 cfv class y
21 1 cv setvar m
22 20 21 wceq wff y = m
23 22 17 18 crab class y ∈ 𝒫 s | y = m
24 15 23 16 co class dom ⁡ r y ∈ 𝒫 s | y = m
25 vc setvar c
26 vx setvar x
27 25 cv setvar c
28 27 14 cfv class r ⁡ c
29 26 cv setvar x
30 29 9 cfv class x
31 28 30 8 wbr wff r ⁡ c ≤ x
32 29 cpw class 𝒫 x
33 13 cv setvar f
34 19 33 cfv class f ⁡ y
35 34 27 wceq wff f ⁡ y = c
36 22 35 wi wff y = m → f ⁡ y = c
37 36 17 32 wral wff ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
38 31 37 wa wff r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
39 38 26 18 wrex wff ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
40 39 25 15 wrex wff ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
41 40 13 24 wral wff ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
42 12 41 wi wff n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
43 42 6 wal wff ∀ s n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
44 43 5 2 crab class n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c
45 cxr class ℝ *
46 clt class <
47 44 45 46 cinf class inf n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c ℝ * <
48 1 3 2 4 47 cmpo class m ∈ ℕ 0 , r ∈ V ⟼ inf n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c ℝ * <
49 0 48 wceq wff Ramsey = m ∈ ℕ 0 , r ∈ V ⟼ inf n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ dom ⁡ r y ∈ 𝒫 s | y = m ∃ c ∈ dom ⁡ r ∃ x ∈ 𝒫 s r ⁡ c ≤ x ∧ ∀ y ∈ 𝒫 x y = m → f ⁡ y = c ℝ * <