limsupcl

Description: Closure of the superior limit. (Contributed by NM, 26-Oct-2005) (Revised by AV, 12-Sep-2020)

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

Step	Hyp	Ref	Expression
1		elex	$⊢ F \in V \to F \in V$
2		df-limsup	$⊢ lim sup = (f \in V ⟼ inf (ran (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
3		eqid	$⊢ (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
4		inss2	$⊢ f [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
5		supxrcl	$⊢ f [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
6	4 5	mp1i	$⊢ k \in ℝ \to sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
7	3 6	fmpti	$⊢ (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) : ℝ ⟶ ℝ^{*}$
8		frn	$⊢ (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) : ℝ ⟶ ℝ^{} \to ran (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{}$
9	7 8	ax-mp	$⊢ ran (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{*}$
10		infxrcl	$⊢ ran (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{} \to inf (ran (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{*}$
11	9 10	mp1i	$⊢ f \in V \to inf (ran (k \in ℝ ⟼ sup (f [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{}$
12	2 11	fmpti	$⊢ lim sup : V ⟶ ℝ^{*}$
13	12	ffvelcdmi	$⊢ F \in V \to lim sup (F) \in ℝ^{*}$
14	1 13	syl	$⊢ F \in V \to lim sup (F) \in ℝ^{*}$

Metamath Proof Explorer