limsuplesup

Description: An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Step	Hyp	Ref	Expression
1		limsuplesup.1	$⊢ φ \to F \in V$
2		limsuplesup.2	$⊢ φ \to K \in ℝ$
3		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
4	3	limsupval	$⊢ F \in V \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
5	1 4	syl	$⊢ φ \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
6		nfv	$⊢ Ⅎ k φ$
7		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
8	7	a1i	$⊢ (φ \land k \in ℝ) \to F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
9	8	supxrcld	$⊢ (φ \land k \in ℝ) \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
10		inss2	$⊢ F [[K, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
11	10	a1i	$⊢ φ \to F [[K, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
12	11	supxrcld	$⊢ φ \to sup (F [[K, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
13		oveq1	$⊢ k = K \to [k, +∞) = [K, +∞)$
14	13	imaeq2d	$⊢ k = K \to F [[k, +∞)] = F [[K, +∞)]$
15	14	ineq1d	$⊢ k = K \to F [[k, +∞)] \cap ℝ^{} = F [[K, +∞)] \cap ℝ^{}$
16	15	supeq1d	$⊢ k = K \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[K, +∞)] \cap ℝ^{} ℝ^{} <)$
17	6 9 2 12 16	infxrlbrnmpt2	$⊢ φ \to inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq sup (F [[K, +∞)] \cap ℝ^{} ℝ^{*} <)$
18	5 17	eqbrtrd	$⊢ φ \to lim sup (F) \leq sup (F [[K, +∞)] \cap ℝ^{} ℝ^{} <)$

Metamath Proof Explorer