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 \in ℕ_{0}, r \in V ⟼ sup (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to 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 \leq$
9		chash	$class \|.\|$
10	6	cv	$setvar s$
11	10 9	cfv	$class \|s\|$
12	7 11 8	wbr	$wff n \leq \|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 \in 𝒫 s \| \|y\| = m\}$
24	15 23 16	co	$class ({dom r}^{\{y \in 𝒫 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) \leq \|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 \to f (y) = c)$
37	36 17 32	wral	$wff \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)$
38	31 37	wa	$wff (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))$
39	38 26 18	wrex	$wff \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))$
40	39 25 15	wrex	$wff \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))$
41	40 13 24	wral	$wff \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))$
42	12 41	wi	$wff (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))$
43	42 6	wal	$wff \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))$
44	43 5 2	crab	$class \{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\}$
45		cxr	$class ℝ^{*}$
46		clt	$class <$
47	44 45 46	cinf	$class sup (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} ℝ^{*} <)$
48	1 3 2 4 47	cmpo	$class (m \in ℕ_{0}, r \in V ⟼ sup (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} ℝ^{*} <))$
49	0 48	wceq	$wff Ramsey = (m \in ℕ_{0}, r \in V ⟼ sup (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} ℝ^{*} <))$

Metamath Proof Explorer

Definition df-ram

Detailed syntax breakdown