liminfgval

Description: Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	liminfgval.1	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	liminfgval	$⊢ M \in ℝ \to G (M) = inf (F [[M, +∞)] \cap ℝ^{} ℝ^{} <)$

Step	Hyp	Ref	Expression
1		liminfgval.1	$⊢ G = (k \in ℝ ⟼ inf (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	infeq1d	$⊢ k = M \to inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = inf (F [[M, +∞)] \cap ℝ^{} ℝ^{} <)$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	infex	$⊢ inf (F [[M, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
8	5 1 7	fvmpt	$⊢ M \in ℝ \to G (M) = inf (F [[M, +∞)] \cap ℝ^{} ℝ^{} <)$

Metamath Proof Explorer