Theorem limsupgval

Description: Value 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	limsupgval	$$⊢M\in ℝ\to G\left(M\right)=sup\left(F\left[\left[M,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$$

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		oveq1	$$⊢k=M\to \left[k,\mathrm{+\infty }\right)=\left[M,\mathrm{+\infty }\right)$$
3	2	imaeq2d	$$⊢k=M\to F\left[\left[k,\mathrm{+\infty }\right)\right]=F\left[\left[M,\mathrm{+\infty }\right)\right]$$
4	3	ineq1d	$$⊢k=M\to F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=F\left[\left[M,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}$$
5	4	supeq1d	$$⊢k=M\to sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)=sup\left(F\left[\left[M,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$$
6		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
7	6	supex	$$⊢sup\left(F\left[\left[M,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\in \mathrm{V}$$
8	5 1 7	fvmpt	$$⊢M\in ℝ\to G\left(M\right)=sup\left(F\left[\left[M,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$$