liminfcl

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

		Ref	Expression
	Assertion	liminfcl	$⊢ F \in V \to lim inf (F) \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2	1	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
3		nfv	$⊢ Ⅎ k F \in V$
4		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
5		infxrcl	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
6	4 5	ax-mp	$⊢ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
7	6	a1i	$⊢ (F \in V \land k \in ℝ) \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
8	3 1 7	rnmptssd	$⊢ F \in V \to ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{*}$
9	8	supxrcld	$⊢ F \in V \to sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{}$
10	2 9	eqeltrd	$⊢ F \in V \to lim inf (F) \in ℝ^{*}$

Metamath Proof Explorer