limsuplt2

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

	Ref	Expression
Hypotheses	limsuplt2.1	$⊢ φ \to B \subseteq ℝ$
	limsuplt2.2	$⊢ φ \to F : B ⟶ ℝ^{*}$
	limsuplt2.3	$⊢ φ \to A \in ℝ^{*}$
Assertion	limsuplt2	$⊢ φ \to (lim sup (F) < A \leftrightarrow \exists k \in ℝ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) < A)$

Proof

Step	Hyp	Ref	Expression
1		limsuplt2.1	$⊢ φ \to B \subseteq ℝ$
2		limsuplt2.2	$⊢ φ \to F : B ⟶ ℝ^{*}$
3		limsuplt2.3	$⊢ φ \to A \in ℝ^{*}$
4		eqid	$⊢ (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) = (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <))$
5	4	limsuplt	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (lim sup (F) < A \leftrightarrow \exists i \in ℝ (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) < A)$
6	1 2 3 5	syl3anc	$⊢ φ \to (lim sup (F) < A \leftrightarrow \exists i \in ℝ (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) < A)$
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	breq1d	$⊢ (φ \land i \in ℝ) \to ((j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) < A \leftrightarrow sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) < A)$
17	16	rexbidva	$⊢ φ \to (\exists i \in ℝ (j \in ℝ ⟼ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)) (i) < A \leftrightarrow \exists i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) < A)$
18		oveq1	$⊢ i = k \to [i, +∞) = [k, +∞)$
19	18	imaeq2d	$⊢ i = k \to F [[i, +∞)] = F [[k, +∞)]$
20	19	ineq1d	$⊢ i = k \to F [[i, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
21	20	supeq1d	$⊢ i = k \to sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
22	21	breq1d	$⊢ i = k \to (sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) < A \leftrightarrow sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) < A)$
23	22	cbvrexvw	$⊢ \exists i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) < A \leftrightarrow \exists k \in ℝ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) < A$
24	23	a1i	$⊢ φ \to (\exists i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) < A \leftrightarrow \exists k \in ℝ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) < A)$
25	6 17 24	3bitrd	$⊢ φ \to (lim sup (F) < A \leftrightarrow \exists k \in ℝ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) < A)$

Metamath Proof Explorer

Theorem limsuplt2

Proof