Metamath Proof Explorer

Theorem ramcl2lem

Description: Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c ${⊢}{C}=\left({a}\in \mathrm{V},{i}\in {ℕ}_{0}⟼\left\{{b}\in 𝒫{a}|\left|{b}\right|={i}\right\}\right)$
ramval.t ${⊢}{T}=\left\{{n}\in {ℕ}_{0}|\forall {s}\phantom{\rule{.4em}{0ex}}\left({n}\le \left|{s}\right|\to \forall {f}\in \left({{R}}^{\left({s}{C}{M}\right)}\right)\phantom{\rule{.4em}{0ex}}\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)\right\}$
Assertion ramcl2lem ${⊢}\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\to {M}\mathrm{Ramsey}{F}=if\left({T}=\varnothing ,\mathrm{+\infty },sup\left({T},ℝ,<\right)\right)$

Proof

Step Hyp Ref Expression
1 ramval.c ${⊢}{C}=\left({a}\in \mathrm{V},{i}\in {ℕ}_{0}⟼\left\{{b}\in 𝒫{a}|\left|{b}\right|={i}\right\}\right)$
2 ramval.t ${⊢}{T}=\left\{{n}\in {ℕ}_{0}|\forall {s}\phantom{\rule{.4em}{0ex}}\left({n}\le \left|{s}\right|\to \forall {f}\in \left({{R}}^{\left({s}{C}{M}\right)}\right)\phantom{\rule{.4em}{0ex}}\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)\right\}$
3 eqeq2 ${⊢}\mathrm{+\infty }=if\left({T}=\varnothing ,\mathrm{+\infty },sup\left({T},ℝ,<\right)\right)\to \left({M}\mathrm{Ramsey}{F}=\mathrm{+\infty }↔{M}\mathrm{Ramsey}{F}=if\left({T}=\varnothing ,\mathrm{+\infty },sup\left({T},ℝ,<\right)\right)\right)$
4 eqeq2 ${⊢}sup\left({T},ℝ,<\right)=if\left({T}=\varnothing ,\mathrm{+\infty },sup\left({T},ℝ,<\right)\right)\to \left({M}\mathrm{Ramsey}{F}=sup\left({T},ℝ,<\right)↔{M}\mathrm{Ramsey}{F}=if\left({T}=\varnothing ,\mathrm{+\infty },sup\left({T},ℝ,<\right)\right)\right)$
5 1 2 ramval ${⊢}\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\to {M}\mathrm{Ramsey}{F}=sup\left({T},{ℝ}^{*},<\right)$
6 infeq1 ${⊢}{T}=\varnothing \to sup\left({T},{ℝ}^{*},<\right)=sup\left(\varnothing ,{ℝ}^{*},<\right)$
7 xrinf0 ${⊢}sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$
8 6 7 syl6eq ${⊢}{T}=\varnothing \to sup\left({T},{ℝ}^{*},<\right)=\mathrm{+\infty }$
9 5 8 sylan9eq ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}=\varnothing \right)\to {M}\mathrm{Ramsey}{F}=\mathrm{+\infty }$
10 df-ne ${⊢}{T}\ne \varnothing ↔¬{T}=\varnothing$
11 5 adantr ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to {M}\mathrm{Ramsey}{F}=sup\left({T},{ℝ}^{*},<\right)$
12 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
13 12 a1i ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to <\mathrm{Or}{ℝ}^{*}$
14 2 ssrab3 ${⊢}{T}\subseteq {ℕ}_{0}$
15 nn0ssre ${⊢}{ℕ}_{0}\subseteq ℝ$
16 14 15 sstri ${⊢}{T}\subseteq ℝ$
17 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
18 14 17 sseqtri ${⊢}{T}\subseteq {ℤ}_{\ge 0}$
19 18 a1i ${⊢}\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\to {T}\subseteq {ℤ}_{\ge 0}$
20 infssuzcl ${⊢}\left({T}\subseteq {ℤ}_{\ge 0}\wedge {T}\ne \varnothing \right)\to sup\left({T},ℝ,<\right)\in {T}$
21 19 20 sylan ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to sup\left({T},ℝ,<\right)\in {T}$
22 16 21 sseldi ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to sup\left({T},ℝ,<\right)\in ℝ$
23 22 rexrd ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to sup\left({T},ℝ,<\right)\in {ℝ}^{*}$
24 22 adantr ${⊢}\left(\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\wedge {z}\in {T}\right)\to sup\left({T},ℝ,<\right)\in ℝ$
25 16 a1i ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to {T}\subseteq ℝ$
26 25 sselda ${⊢}\left(\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\wedge {z}\in {T}\right)\to {z}\in ℝ$
27 simpr ${⊢}\left(\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\wedge {z}\in {T}\right)\to {z}\in {T}$
28 infssuzle ${⊢}\left({T}\subseteq {ℤ}_{\ge 0}\wedge {z}\in {T}\right)\to sup\left({T},ℝ,<\right)\le {z}$
29 18 27 28 sylancr ${⊢}\left(\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\wedge {z}\in {T}\right)\to sup\left({T},ℝ,<\right)\le {z}$
30 24 26 29 lensymd ${⊢}\left(\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\wedge {z}\in {T}\right)\to ¬{z}
31 13 23 21 30 infmin ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to sup\left({T},{ℝ}^{*},<\right)=sup\left({T},ℝ,<\right)$
32 11 31 eqtrd ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge {T}\ne \varnothing \right)\to {M}\mathrm{Ramsey}{F}=sup\left({T},ℝ,<\right)$
33 10 32 sylan2br ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\wedge ¬{T}=\varnothing \right)\to {M}\mathrm{Ramsey}{F}=sup\left({T},ℝ,<\right)$
34 3 4 9 33 ifbothda ${⊢}\left({M}\in {ℕ}_{0}\wedge {R}\in {V}\wedge {F}:{R}⟶{ℕ}_{0}\right)\to {M}\mathrm{Ramsey}{F}=if\left({T}=\varnothing ,\mathrm{+\infty },sup\left({T},ℝ,<\right)\right)$