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 = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	limsupgval	$⊢ M \in ℝ \to G (M) = sup (F [[M, +∞)] \cap ℝ^{} ℝ^{} <)$

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		oveq1	$⊢ k = M \to [k, +∞) = [M, +∞)$
3	2	imaeq2d	$⊢ k = M \to F [[k, +∞)] = F [[M, +∞)]$
4	3	ineq1d	$⊢ k = M \to F [[k, +∞)] \cap ℝ^{} = F [[M, +∞)] \cap ℝ^{}$
5	4	supeq1d	$⊢ k = M \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[M, +∞)] \cap ℝ^{} ℝ^{} <)$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	supex	$⊢ sup (F [[M, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
8	5 1 7	fvmpt	$⊢ M \in ℝ \to G (M) = sup (F [[M, +∞)] \cap ℝ^{} ℝ^{} <)$

Metamath Proof Explorer