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

Detailed syntax breakdown

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