limsupge

Description: The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	limsupge.b	$⊢ φ \to B \subseteq ℝ$
	limsupge.f	$⊢ φ \to F : B ⟶ ℝ^{*}$
	limsupge.a	$⊢ φ \to A \in ℝ^{*}$
Assertion	limsupge	$⊢ φ \to (A \leq lim sup (F) \leftrightarrow \forall k \in ℝ A \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$

Proof

Step	Hyp	Ref	Expression
1		limsupge.b	$⊢ φ \to B \subseteq ℝ$
2		limsupge.f	$⊢ φ \to F : B ⟶ ℝ^{*}$
3		limsupge.a	$⊢ φ \to A \in ℝ^{*}$
4		eqid	$⊢ (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) = (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <))$
5	4	limsuple	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq lim sup (F) \leftrightarrow \forall i \in ℝ A \leq (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i))$
6	1 2 3 5	syl3anc	$⊢ φ \to (A \leq lim sup (F) \leftrightarrow \forall i \in ℝ A \leq (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i))$
7		oveq1	$⊢ j = i \to [j, +∞) = [i, +∞)$
8	7	imaeq2d	$⊢ j = i \to F [[j, +∞)] = F [[i, +∞)]$
9	8	ineq1d	$⊢ j = i \to F [[j, +∞)] \cap ℝ^{} = F [[i, +∞)] \cap ℝ^{}$
10	9	supeq1d	$⊢ j = i \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)$
11		simpr	$⊢ (φ \land i \in ℝ) \to i \in ℝ$
12		xrltso	$⊢ < Or ℝ^{*}$
13	12	supex	$⊢ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
14	13	a1i	$⊢ (φ \land i \in ℝ) \to sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
15	4 10 11 14	fvmptd3	$⊢ (φ \land i \in ℝ) \to (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) = sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)$
16	15	breq2d	$⊢ (φ \land i \in ℝ) \to (A \leq (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) \leftrightarrow A \leq sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
17	16	ralbidva	$⊢ φ \to (\forall i \in ℝ A \leq (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) \leftrightarrow \forall i \in ℝ A \leq sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
18	6 17	bitrd	$⊢ φ \to (A \leq lim sup (F) \leftrightarrow \forall i \in ℝ A \leq sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
19		oveq1	$⊢ i = k \to [i, +∞) = [k, +∞)$
20	19	imaeq2d	$⊢ i = k \to F [[i, +∞)] = F [[k, +∞)]$
21	20	ineq1d	$⊢ i = k \to F [[i, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
22	21	supeq1d	$⊢ i = k \to sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
23	22	breq2d	$⊢ i = k \to (A \leq sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leftrightarrow A \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
24	23	cbvralvw	$⊢ \forall i \in ℝ A \leq sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leftrightarrow \forall k \in ℝ A \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
25	24	a1i	$⊢ φ \to (\forall i \in ℝ A \leq sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leftrightarrow \forall k \in ℝ A \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
26	18 25	bitrd	$⊢ φ \to (A \leq lim sup (F) \leftrightarrow \forall k \in ℝ A \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$

Metamath Proof Explorer

Theorem limsupge

Proof