liminfval

Description: The inferior limit of a set F . (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	liminfval.1	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran G ℝ^{*} <)$

Step	Hyp	Ref	Expression
1		liminfval.1	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		df-liminf	$⊢ lim inf = (x \in V ⟼ sup (ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
3		imaeq1	$⊢ x = F \to x [[k, +∞)] = F [[k, +∞)]$
4	3	ineq1d	$⊢ x = F \to x [[k, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
5	4	infeq1d	$⊢ x = F \to inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <) = inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
6	5	mpteq2dv	$⊢ x = F \to (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
7	1	a1i	$⊢ x = F \to G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
8	6 7	eqtr4d	$⊢ x = F \to (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = G$
9	8	rneqd	$⊢ x = F \to ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran G$
10	9	supeq1d	$⊢ x = F \to sup (ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = sup (ran G ℝ^{} <)$
11		elex	$⊢ F \in V \to F \in V$
12		xrltso	$⊢ < Or ℝ^{*}$
13	12	supex	$⊢ sup (ran G ℝ^{*} <) \in V$
14	13	a1i	$⊢ F \in V \to sup (ran G ℝ^{*} <) \in V$
15	2 10 11 14	fvmptd3	$⊢ F \in V \to lim inf (F) = sup (ran G ℝ^{*} <)$

Metamath Proof Explorer