Theorem limsupgf

Description: Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

	Ref	Expression
Hypothesis	limsupval.1	$$⊢G=\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
Assertion	limsupgf	$$⊢G:ℝ⟶{ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$$⊢G=\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
2		inss2	$$⊢F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\subseteq {ℝ}^{*}$$
3		supxrcl	$$⊢F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\subseteq {ℝ}^{*}\to sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
4	2 3	mp1i	$$⊢k\in ℝ\to sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
5	1 4	fmpti	$$⊢G:ℝ⟶{ℝ}^{*}$$