# Metamath Proof Explorer

## Theorem limsupval3

Description: The superior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupval3.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
limsupval3.2 ${⊢}{\phi }\to {A}\in {V}$
limsupval3.3 ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{*}$
limsupval3.4 ${⊢}{G}=\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)$
Assertion limsupval3 ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}{G},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 limsupval3.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 limsupval3.2 ${⊢}{\phi }\to {A}\in {V}$
3 limsupval3.3 ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{*}$
4 limsupval3.4 ${⊢}{G}=\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)$
5 3 2 fexd ${⊢}{\phi }\to {F}\in \mathrm{V}$
6 eqid ${⊢}\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$
7 6 limsupval ${⊢}{F}\in \mathrm{V}\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$
8 5 7 syl ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$
9 4 a1i ${⊢}{\phi }\to {G}=\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)$
10 3 fimassd ${⊢}{\phi }\to {F}\left[\left[{k},\mathrm{+\infty }\right)\right]\subseteq {ℝ}^{*}$
11 df-ss ${⊢}{F}\left[\left[{k},\mathrm{+\infty }\right)\right]\subseteq {ℝ}^{*}↔{F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}={F}\left[\left[{k},\mathrm{+\infty }\right)\right]$
12 10 11 sylib ${⊢}{\phi }\to {F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}={F}\left[\left[{k},\mathrm{+\infty }\right)\right]$
13 12 eqcomd ${⊢}{\phi }\to {F}\left[\left[{k},\mathrm{+\infty }\right)\right]={F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}$
14 13 supeq1d ${⊢}{\phi }\to sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)=sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$
15 14 adantr ${⊢}\left({\phi }\wedge {k}\in ℝ\right)\to sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)=sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$
16 1 15 mpteq2da ${⊢}{\phi }\to \left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$
17 9 16 eqtr2d ${⊢}{\phi }\to \left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)={G}$
18 17 rneqd ${⊢}{\phi }\to \mathrm{ran}\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\mathrm{ran}{G}$
19 18 infeq1d ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({F}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}{G},{ℝ}^{*},<\right)$
20 8 19 eqtrd ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}{G},{ℝ}^{*},<\right)$