liminfval5

Description: The inferior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		limsupval5.1	$⊢ Ⅎ k φ$
2		limsupval5.2	$⊢ φ \to A \in V$
3		limsupval5.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
4		limsupval5.4	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] ℝ^{*} <))$
5	3 2	fexd	$⊢ φ \to F \in V$
6		eqid	$⊢ (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
7	6	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
8	5 7	syl	$⊢ φ \to lim inf (F) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
9	4	a1i	$⊢ φ \to G = (k \in ℝ ⟼ inf (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	adantr	$⊢ (φ \land k \in ℝ) \to F [[k, +∞)] = F [[k, +∞)] \cap ℝ^{*}$
15	14	infeq1d	$⊢ (φ \land k \in ℝ) \to inf (F [[k, +∞)] ℝ^{} <) = inf (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
16	1 15	mpteq2da	$⊢ φ \to (k \in ℝ ⟼ inf (F [[k, +∞)] ℝ^{} <)) = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <))$
17	9 16	eqtr2d	$⊢ φ \to (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = G$
18	17	rneqd	$⊢ φ \to ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran G$
19	18	supeq1d	$⊢ φ \to sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = sup (ran G ℝ^{} <)$
20	8 19	eqtrd	$⊢ φ \to lim inf (F) = sup (ran G ℝ^{*} <)$

Metamath Proof Explorer

Theorem liminfval5

Proof