limsupval3

Description: The superior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupval3.1	$⊢ Ⅎ k φ$
	limsupval3.2	$⊢ φ \to A \in V$
	limsupval3.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
	limsupval3.4	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{*} <))$
Assertion	limsupval3	$⊢ φ \to lim sup (F) = inf (ran G ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		limsupval3.1	$⊢ Ⅎ k φ$
2		limsupval3.2	$⊢ φ \to A \in V$
3		limsupval3.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
4		limsupval3.4	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{*} <))$
5	3 2	fexd	$⊢ φ \to F \in V$
6		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
7	6	limsupval	$⊢ F \in V \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
8	5 7	syl	$⊢ φ \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
9	4	a1i	$⊢ φ \to G = (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{*} <))$
10	3	fimassd	$⊢ φ \to F [[k, +∞)] \subseteq ℝ^{*}$
11		dfss2	$⊢ F [[k, +∞)] \subseteq ℝ^{} \leftrightarrow F [[k, +∞)] \cap ℝ^{} = F [[k, +∞)]$
12	10 11	sylib	$⊢ φ \to F [[k, +∞)] \cap ℝ^{*} = F [[k, +∞)]$
13	12	eqcomd	$⊢ φ \to F [[k, +∞)] = F [[k, +∞)] \cap ℝ^{*}$
14	13	supeq1d	$⊢ φ \to sup (F [[k, +∞)] ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
15	14	adantr	$⊢ (φ \land k \in ℝ) \to sup (F [[k, +∞)] ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
16	1 15	mpteq2da	$⊢ φ \to (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <))$
17	9 16	eqtr2d	$⊢ φ \to (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = G$
18	17	rneqd	$⊢ φ \to ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran G$
19	18	infeq1d	$⊢ φ \to inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = inf (ran G ℝ^{} <)$
20	8 19	eqtrd	$⊢ φ \to lim sup (F) = inf (ran G ℝ^{*} <)$

Metamath Proof Explorer

Theorem limsupval3

Proof