Theorem ramval 16754

Description: The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 14-Sep-2020.)

Hypotheses

Ref	Expression
ramval.c	⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})
ramval.t	⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}

Assertion

Ref	Expression
ramval	⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, < ))

Distinct variable groups:   𝑓,𝑐,𝑥,𝐶   𝑛,𝑐,𝑠,𝐹,𝑓,𝑥   𝑎,𝑏,𝑐,𝑓,𝑖,𝑛,𝑠,𝑥,𝑀   𝑅,𝑐,𝑓,𝑛,𝑠,𝑥   𝑉,𝑐,𝑓,𝑛,𝑠,𝑥

Allowed substitution hints:   𝐶(𝑖,𝑛,𝑠,𝑎,𝑏)   𝑅(𝑖,𝑎,𝑏)   𝑇(𝑥,𝑓,𝑖,𝑛,𝑠,𝑎,𝑏,𝑐)   𝐹(𝑖,𝑎,𝑏)   𝑉(𝑖,𝑎,𝑏)

Proof of Theorem ramval

Dummy variables 𝑦 𝑚 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ram 16747	. . 3 ⊢ Ramsey = (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ))
2	1	a1i 11	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → Ramsey = (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < )))
3		simplrr 776	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑟 = 𝐹)
4	3	dmeqd 5827	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝑟 = dom 𝐹)
5		simpll3 1214	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝐹:𝑅⟶ℕ0)
6	5	fdmd 6641	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝐹 = 𝑅)
7	4, 6	eqtrd 2776	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → dom 𝑟 = 𝑅)
8		simplrl 775	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑚 = 𝑀)
9	8	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → ((♯‘𝑦) = 𝑚 ↔ (♯‘𝑦) = 𝑀))
10	9	rabbidv 3421	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚} = {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑀})
11		vex 3441	. . . . . . . . . . . 12 ⊢ 𝑠 ∈ V
12		simpll1 1212	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ ℕ0)
13		ramval.c	. . . . . . . . . . . . 13 ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})
14	13	hashbcval 16748	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ V ∧ 𝑀 ∈ ℕ0) → (𝑠𝐶𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑀})
15	11, 12, 14	sylancr 588	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (𝑠𝐶𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑀})
16	10, 15	eqtr4d 2779	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚} = (𝑠𝐶𝑀))
17	7, 16	oveq12d 7325	. . . . . . . . 9 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚}) = (𝑅 ↑m (𝑠𝐶𝑀)))
18	17	raleqdv 3360	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))))
19		simpr 486	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑀 ∧ 𝑟 = 𝐹) → 𝑟 = 𝐹)
20	19	dmeqd 5827	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑟 = 𝐹) → dom 𝑟 = dom 𝐹)
21		fdm 6639	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑅⟶ℕ0 → dom 𝐹 = 𝑅)
22	21	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → dom 𝐹 = 𝑅)
23	20, 22	sylan9eqr 2798	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → dom 𝑟 = 𝑅)
24	23	ad2antrr 724	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) → dom 𝑟 = 𝑅)
25	3	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑟 = 𝐹)
26	25	fveq1d 6806	. . . . . . . . . . . . 13 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑟‘𝑐) = (𝐹‘𝑐))
27	26	breq1d 5091	. . . . . . . . . . . 12 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ((𝑟‘𝑐) ≤ (♯‘𝑥) ↔ (𝐹‘𝑐) ≤ (♯‘𝑥)))
28	8	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑚 = 𝑀)
29	28	oveq2d 7323	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑚) = (𝑥𝐶𝑀))
30		vex 3441	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
31	12	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑀 ∈ ℕ0)
32	28, 31	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑚 ∈ ℕ0)
33	13	hashbcval 16748	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ 𝑚 ∈ ℕ0) → (𝑥𝐶𝑚) = {𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚})
34	30, 32, 33	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑚) = {𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚})
35	29, 34	eqtr3d 2778	. . . . . . . . . . . . . 14 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑀) = {𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚})
36	35	sseq1d 3957	. . . . . . . . . . . . 13 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ((𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}) ↔ {𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐})))
37		rabss 4011	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}) ↔ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})))
38	35	eleq2d 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑦 ∈ (𝑥𝐶𝑀) ↔ 𝑦 ∈ {𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚}))
39		rabid 3322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚} ↔ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚))
40	38, 39	bitrdi 287	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑦 ∈ (𝑥𝐶𝑀) ↔ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚)))
41	40	biimpar 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚)) → 𝑦 ∈ (𝑥𝐶𝑀))
42		elpwi 4546	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝒫 𝑠 → 𝑥 ⊆ 𝑠)
43	42	adantl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → 𝑥 ⊆ 𝑠)
44	13	hashbcss 16750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ∈ V ∧ 𝑥 ⊆ 𝑠 ∧ 𝑀 ∈ ℕ0) → (𝑥𝐶𝑀) ⊆ (𝑠𝐶𝑀))
45	11, 43, 31, 44	mp3an2i 1466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥𝐶𝑀) ⊆ (𝑠𝐶𝑀))
46	45	sselda 3926	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ (𝑥𝐶𝑀)) → 𝑦 ∈ (𝑠𝐶𝑀))
47	41, 46	syldan 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚)) → 𝑦 ∈ (𝑠𝐶𝑀))
48		elmapi 8668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀)) → 𝑓:(𝑠𝐶𝑀)⟶𝑅)
49	48	ad3antlr 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚)) → 𝑓:(𝑠𝐶𝑀)⟶𝑅)
50		ffn 6630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(𝑠𝐶𝑀)⟶𝑅 → 𝑓 Fn (𝑠𝐶𝑀))
51		fniniseg 6969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 Fn (𝑠𝐶𝑀) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐)))
52	49, 50, 51	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚)) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐶𝑀) ∧ (𝑓‘𝑦) = 𝑐)))
53	47, 52	mpbirand 705	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 𝑥 ∧ (♯‘𝑦) = 𝑚)) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑓‘𝑦) = 𝑐))
54	53	anassrs 469	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 𝑥) ∧ (♯‘𝑦) = 𝑚) → (𝑦 ∈ (◡𝑓 “ {𝑐}) ↔ (𝑓‘𝑦) = 𝑐))
55	54	pm5.74da 802	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 𝑥) → (((♯‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})) ↔ ((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))
56	55	ralbidva 3169	. . . . . . . . . . . . . 14 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → 𝑦 ∈ (◡𝑓 “ {𝑐})) ↔ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))
57	37, 56	bitrid 283	. . . . . . . . . . . . 13 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → ({𝑦 ∈ 𝒫 𝑥 ∣ (♯‘𝑦) = 𝑚} ⊆ (◡𝑓 “ {𝑐}) ↔ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))
58	36, 57	bitr2d 280	. . . . . . . . . . . 12 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐) ↔ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))
59	27, 58	anbi12d 632	. . . . . . . . . . 11 ⊢ ((((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) ∧ 𝑥 ∈ 𝒫 𝑠) → (((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))
60	59	rexbidva 3170	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) → (∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))
61	24, 60	rexeqbidv 3349	. . . . . . . . 9 ⊢ (((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))) → (∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))
62	61	ralbidva 3169	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))
63	18, 62	bitrd 279	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)) ↔ ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))
64	63	imbi2d 341	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) ↔ (𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))))
65	64	albidv 1921	. . . . 5 ⊢ ((((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) ∧ 𝑛 ∈ ℕ0) → (∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐))) ↔ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))))
66	65	rabbidva 3420	. . . 4 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))} = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))})
67		ramval.t	. . . 4 ⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}
68	66, 67	eqtr4di 2794	. . 3 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))} = 𝑇)
69	68	infeq1d 9280	. 2 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑚 = 𝑀 ∧ 𝑟 = 𝐹)) → inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ) = inf(𝑇, ℝ*, < ))
70		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝑀 ∈ ℕ0)
71		simp3 1138	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝐹:𝑅⟶ℕ0)
72		simp2 1137	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝑅 ∈ 𝑉)
73	71, 72	fexd 7135	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → 𝐹 ∈ V)
74		xrltso 12921	. . . 4 ⊢ < Or ℝ*
75	74	infex 9296	. . 3 ⊢ inf(𝑇, ℝ*, < ) ∈ V
76	75	a1i 11	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → inf(𝑇, ℝ*, < ) ∈ V)
77	2, 69, 70, 73, 76	ovmpod 7457	1 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, < ))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1087  ∀wal 1537   = wceq 1539   ∈ wcel 2104  ∀wral 3062  ∃wrex 3071  {crab 3284  Vcvv 3437   ⊆ wss 3892  𝒫 cpw 4539  {csn 4565   class class class wbr 5081  ^◡ccnv 5599  dom cdm 5600   “ cima 5603   Fn wfn 6453  ⟶wf 6454  ‘cfv 6458  (class class class)co 7307   ∈ cmpo 7309   ↑_m cmap 8646  infcinf 9244  ℝ^*cxr 11054   < clt 11055   ≤ cle 11056  ℕ₀cn0 12279  ♯chash 14090   Ramsey cram 16745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10973  ax-resscn 10974  ax-pre-lttri 10991  ax-pre-lttrn 10992

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-po 5514  df-so 5515  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-oprab 7311  df-mpo 7312  df-1st 7863  df-2nd 7864  df-er 8529  df-map 8648  df-en 8765  df-dom 8766  df-sdom 8767  df-sup 9245  df-inf 9246  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-ram 16747

This theorem is referenced by:  ramcl2lem  16755