# Metamath Proof Explorer

## 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 ${⊢}{C}=\left({a}\in \mathrm{V},{i}\in {ℕ}_{0}⟼\left\{{b}\in 𝒫{a}|\left|{b}\right|={i}\right\}\right)$
rami.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
rami.r ${⊢}{\phi }\to {R}\in {V}$
rami.f ${⊢}{\phi }\to {F}:{R}⟶{ℕ}_{0}$
ramub2.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
ramub2.i ${⊢}\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge {f}:{s}{C}{M}⟶{R}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]\right)$
Assertion ramub2 ${⊢}{\phi }\to {M}\mathrm{Ramsey}{F}\le {N}$

### Proof

Step Hyp Ref Expression
1 rami.c ${⊢}{C}=\left({a}\in \mathrm{V},{i}\in {ℕ}_{0}⟼\left\{{b}\in 𝒫{a}|\left|{b}\right|={i}\right\}\right)$
2 rami.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
3 rami.r ${⊢}{\phi }\to {R}\in {V}$
4 rami.f ${⊢}{\phi }\to {F}:{R}⟶{ℕ}_{0}$
5 ramub2.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
6 ramub2.i ${⊢}\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge {f}:{s}{C}{M}⟶{R}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]\right)$
7 5 adantr ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to {N}\in {ℕ}_{0}$
8 hashfz1 ${⊢}{N}\in {ℕ}_{0}\to \left|\left(1\dots {N}\right)\right|={N}$
9 7 8 syl ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \left|\left(1\dots {N}\right)\right|={N}$
10 simprl ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to {N}\le \left|{t}\right|$
11 9 10 eqbrtrd ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \left|\left(1\dots {N}\right)\right|\le \left|{t}\right|$
12 fzfid ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \left(1\dots {N}\right)\in \mathrm{Fin}$
13 vex ${⊢}{t}\in \mathrm{V}$
14 hashdom ${⊢}\left(\left(1\dots {N}\right)\in \mathrm{Fin}\wedge {t}\in \mathrm{V}\right)\to \left(\left|\left(1\dots {N}\right)\right|\le \left|{t}\right|↔\left(1\dots {N}\right)\preccurlyeq {t}\right)$
15 12 13 14 sylancl ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \left(\left|\left(1\dots {N}\right)\right|\le \left|{t}\right|↔\left(1\dots {N}\right)\preccurlyeq {t}\right)$
16 11 15 mpbid ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \left(1\dots {N}\right)\preccurlyeq {t}$
17 13 domen ${⊢}\left(1\dots {N}\right)\preccurlyeq {t}↔\exists {s}\phantom{\rule{.4em}{0ex}}\left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)$
18 16 17 sylib ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \exists {s}\phantom{\rule{.4em}{0ex}}\left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)$
19 simpll ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {\phi }$
20 ensym ${⊢}\left(1\dots {N}\right)\approx {s}\to {s}\approx \left(1\dots {N}\right)$
21 20 ad2antrl ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {s}\approx \left(1\dots {N}\right)$
22 hasheni ${⊢}{s}\approx \left(1\dots {N}\right)\to \left|{s}\right|=\left|\left(1\dots {N}\right)\right|$
23 21 22 syl ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left|{s}\right|=\left|\left(1\dots {N}\right)\right|$
24 5 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {N}\in {ℕ}_{0}$
25 24 8 syl ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left|\left(1\dots {N}\right)\right|={N}$
26 23 25 eqtrd ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left|{s}\right|={N}$
27 simplrr ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {g}:{t}{C}{M}⟶{R}$
28 simprr ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {s}\subseteq {t}$
29 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {M}\in {ℕ}_{0}$
30 1 hashbcss ${⊢}\left({t}\in \mathrm{V}\wedge {s}\subseteq {t}\wedge {M}\in {ℕ}_{0}\right)\to {s}{C}{M}\subseteq {t}{C}{M}$
31 13 28 29 30 mp3an2i ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to {s}{C}{M}\subseteq {t}{C}{M}$
32 27 31 fssresd ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left({{g}↾}_{\left({s}{C}{M}\right)}\right):{s}{C}{M}⟶{R}$
33 vex ${⊢}{g}\in \mathrm{V}$
34 33 resex ${⊢}{{g}↾}_{\left({s}{C}{M}\right)}\in \mathrm{V}$
35 feq1 ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left({f}:{s}{C}{M}⟶{R}↔\left({{g}↾}_{\left({s}{C}{M}\right)}\right):{s}{C}{M}⟶{R}\right)$
36 35 anbi2d ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left(\left(\left|{s}\right|={N}\wedge {f}:{s}{C}{M}⟶{R}\right)↔\left(\left|{s}\right|={N}\wedge \left({{g}↾}_{\left({s}{C}{M}\right)}\right):{s}{C}{M}⟶{R}\right)\right)$
37 36 anbi2d ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left(\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge {f}:{s}{C}{M}⟶{R}\right)\right)↔\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge \left({{g}↾}_{\left({s}{C}{M}\right)}\right):{s}{C}{M}⟶{R}\right)\right)\right)$
38 cnveq ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to {{f}}^{-1}={\left({{g}↾}_{\left({s}{C}{M}\right)}\right)}^{-1}$
39 38 imaeq1d ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to {{f}}^{-1}\left[\left\{{c}\right\}\right]={\left({{g}↾}_{\left({s}{C}{M}\right)}\right)}^{-1}\left[\left\{{c}\right\}\right]$
40 cnvresima ${⊢}{\left({{g}↾}_{\left({s}{C}{M}\right)}\right)}^{-1}\left[\left\{{c}\right\}\right]={{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)$
41 39 40 syl6eq ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to {{f}}^{-1}\left[\left\{{c}\right\}\right]={{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)$
42 41 sseq2d ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left({x}{C}{M}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]↔{x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)$
43 42 anbi2d ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left(\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]\right)↔\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\right)$
44 43 2rexbidv ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left(\exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]\right)↔\exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\right)$
45 37 44 imbi12d ${⊢}{f}={{g}↾}_{\left({s}{C}{M}\right)}\to \left(\left(\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge {f}:{s}{C}{M}⟶{R}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]\right)\right)↔\left(\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge \left({{g}↾}_{\left({s}{C}{M}\right)}\right):{s}{C}{M}⟶{R}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\right)\right)$
46 34 45 6 vtocl ${⊢}\left({\phi }\wedge \left(\left|{s}\right|={N}\wedge \left({{g}↾}_{\left({s}{C}{M}\right)}\right):{s}{C}{M}⟶{R}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)$
47 19 26 32 46 syl12anc ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)$
48 sstr ${⊢}\left({x}\subseteq {s}\wedge {s}\subseteq {t}\right)\to {x}\subseteq {t}$
49 48 expcom ${⊢}{s}\subseteq {t}\to \left({x}\subseteq {s}\to {x}\subseteq {t}\right)$
50 49 ad2antll ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left({x}\subseteq {s}\to {x}\subseteq {t}\right)$
51 velpw ${⊢}{x}\in 𝒫{s}↔{x}\subseteq {s}$
52 velpw ${⊢}{x}\in 𝒫{t}↔{x}\subseteq {t}$
53 50 51 52 3imtr4g ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left({x}\in 𝒫{s}\to {x}\in 𝒫{t}\right)$
54 id ${⊢}{x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\to {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)$
55 inss1 ${⊢}{{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]$
56 54 55 sstrdi ${⊢}{x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\to {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]$
57 56 a1i ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left({x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\to {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)$
58 57 anim2d ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left(\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\to \left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)\right)$
59 53 58 anim12d ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left(\left({x}\in 𝒫{s}\wedge \left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\right)\to \left({x}\in 𝒫{t}\wedge \left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)\right)\right)$
60 59 reximdv2 ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left(\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\to \exists {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)\right)$
61 60 reximdv ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \left(\exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\cap \left({s}{C}{M}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)\right)$
62 47 61 mpd ${⊢}\left(\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\wedge \left(\left(1\dots {N}\right)\approx {s}\wedge {s}\subseteq {t}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)$
63 18 62 exlimddv ${⊢}\left({\phi }\wedge \left({N}\le \left|{t}\right|\wedge {g}:{t}{C}{M}⟶{R}\right)\right)\to \exists {c}\in {R}\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\le \left|{x}\right|\wedge {x}{C}{M}\subseteq {{g}}^{-1}\left[\left\{{c}\right\}\right]\right)$
64 1 2 3 4 5 63 ramub ${⊢}{\phi }\to {M}\mathrm{Ramsey}{F}\le {N}$