Theorem ramub2

Description: It is sufficient to check the Ramsey property on finite sets of size equal to the upper bound. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	rami.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
	rami.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	rami.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	rami.f	⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
	ramub2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	ramub2.i	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
Assertion	ramub2	⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		rami.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		rami.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3		rami.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4		rami.f	⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
5		ramub2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		ramub2.i	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
7	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → 𝑁 ∈ ℕ0 )
8		hashfz1	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
9	7 8	syl	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → 𝑁 ≤ ( ♯ ‘ 𝑡 ) )
11	9 10	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ( ♯ ‘ ( 1 ... 𝑁 ) ) ≤ ( ♯ ‘ 𝑡 ) )
12		fzfid	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
13		vex	⊢ 𝑡 ∈ V
14		hashdom	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑡 ∈ V ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) ≤ ( ♯ ‘ 𝑡 ) ↔ ( 1 ... 𝑁 ) ≼ 𝑡 ) )
15	12 13 14	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) ≤ ( ♯ ‘ 𝑡 ) ↔ ( 1 ... 𝑁 ) ≼ 𝑡 ) )
16	11 15	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ( 1 ... 𝑁 ) ≼ 𝑡 )
17	13	domen	⊢ ( ( 1 ... 𝑁 ) ≼ 𝑡 ↔ ∃ 𝑠 ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) )
18	16 17	sylib	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑠 ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) )
19		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → 𝜑 )
20		ensym	⊢ ( ( 1 ... 𝑁 ) ≈ 𝑠 → 𝑠 ≈ ( 1 ... 𝑁 ) )
21	20	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → 𝑠 ≈ ( 1 ... 𝑁 ) )
22		hasheni	⊢ ( 𝑠 ≈ ( 1 ... 𝑁 ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) )
23	21 22	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) )
24	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → 𝑁 ∈ ℕ0 )
25	24 8	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
26	23 25	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ♯ ‘ 𝑠 ) = 𝑁 )
27		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 )
28		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → 𝑠 ⊆ 𝑡 )
29	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → 𝑀 ∈ ℕ0 )
30	1	hashbcss	⊢ ( ( 𝑡 ∈ V ∧ 𝑠 ⊆ 𝑡 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑠 𝐶 𝑀 ) ⊆ ( 𝑡 𝐶 𝑀 ) )
31	13 28 29 30	mp3an2i	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( 𝑠 𝐶 𝑀 ) ⊆ ( 𝑡 𝐶 𝑀 ) )
32	27 31	fssresd	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 )
33		vex	⊢ 𝑔 ∈ V
34	33	resex	⊢ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) ∈ V
35		feq1	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ↔ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) )
36	35	anbi2d	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ↔ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) )
37	36	anbi2d	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) ↔ ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) ) )
38		cnveq	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ◡ 𝑓 = ◡ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) )
39	38	imaeq1d	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) “ { 𝑐 } ) )
40		cnvresima	⊢ ( ◡ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) “ { 𝑐 } ) = ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) )
41	39 40	eqtrdi	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ◡ 𝑓 “ { 𝑐 } ) = ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) )
42	41	sseq2d	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) )
43	42	anbi2d	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) ) )
44	43	2rexbidv	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) ) )
45	37 44	imbi12d	⊢ ( 𝑓 = ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) → ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ↔ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) ) ) )
46	34 45 6	vtocl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = 𝑁 ∧ ( 𝑔 ↾ ( 𝑠 𝐶 𝑀 ) ) : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) )
47	19 26 32 46	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) )
48		sstr	⊢ ( ( 𝑥 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) → 𝑥 ⊆ 𝑡 )
49	48	expcom	⊢ ( 𝑠 ⊆ 𝑡 → ( 𝑥 ⊆ 𝑠 → 𝑥 ⊆ 𝑡 ) )
50	49	ad2antll	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( 𝑥 ⊆ 𝑠 → 𝑥 ⊆ 𝑡 ) )
51		velpw	⊢ ( 𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠 )
52		velpw	⊢ ( 𝑥 ∈ 𝒫 𝑡 ↔ 𝑥 ⊆ 𝑡 )
53	50 51 52	3imtr4g	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( 𝑥 ∈ 𝒫 𝑠 → 𝑥 ∈ 𝒫 𝑡 ) )
54		id	⊢ ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) → ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) )
55		inss1	⊢ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ⊆ ( ◡ 𝑔 “ { 𝑐 } )
56	54 55	sstrdi	⊢ ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) → ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) )
57	56	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) → ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) )
58	57	anim2d	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) → ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) ) )
59	53 58	anim12d	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ( 𝑥 ∈ 𝒫 𝑠 ∧ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) ) → ( 𝑥 ∈ 𝒫 𝑡 ∧ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) ) ) )
60	59	reximdv2	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) → ∃ 𝑥 ∈ 𝒫 𝑡 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) ) )
61	60	reximdv	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ( ◡ 𝑔 “ { 𝑐 } ) ∩ ( 𝑠 𝐶 𝑀 ) ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑡 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) ) )
62	47 61	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) ∧ ( ( 1 ... 𝑁 ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝑡 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑡 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) )
63	18 62	exlimddv	⊢ ( ( 𝜑 ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑡 ) ∧ 𝑔 : ( 𝑡 𝐶 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑡 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑔 “ { 𝑐 } ) ) )
64	1 2 3 4 5 63	ramub	⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 )