limsuplt

Description: The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

		Ref	Expression
	Hypothesis	limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	limsuplt	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (lim sup (F) < A \leftrightarrow \exists j \in ℝ G (j) < A)$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2	1	limsuple	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq lim sup (F) \leftrightarrow \forall j \in ℝ A \leq G (j))$
3	2	notbid	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (\neg A \leq lim sup (F) \leftrightarrow \neg \forall j \in ℝ A \leq G (j))$
4		rexnal	$⊢ \exists j \in ℝ \neg A \leq G (j) \leftrightarrow \neg \forall j \in ℝ A \leq G (j)$
5	3 4	bitr4di	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (\neg A \leq lim sup (F) \leftrightarrow \exists j \in ℝ \neg A \leq G (j))$
6		simp2	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to F : B ⟶ ℝ^{*}$
7		reex	$⊢ ℝ \in V$
8	7	ssex	$⊢ B \subseteq ℝ \to B \in V$
9	8	3ad2ant1	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to B \in V$
10		xrex	$⊢ ℝ^{*} \in V$
11	10	a1i	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to ℝ^{*} \in V$
12		fex2	$⊢ (F : B ⟶ ℝ^{} \land B \in V \land ℝ^{} \in V) \to F \in V$
13	6 9 11 12	syl3anc	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to F \in V$
14		limsupcl	$⊢ F \in V \to lim sup (F) \in ℝ^{*}$
15	13 14	syl	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to lim sup (F) \in ℝ^{*}$
16		simp3	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to A \in ℝ^{*}$
17		xrltnle	$⊢ (lim sup (F) \in ℝ^{} \land A \in ℝ^{}) \to (lim sup (F) < A \leftrightarrow \neg A \leq lim sup (F))$
18	15 16 17	syl2anc	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (lim sup (F) < A \leftrightarrow \neg A \leq lim sup (F))$
19	1	limsupgf	$⊢ G : ℝ ⟶ ℝ^{*}$
20	19	ffvelcdmi	$⊢ j \in ℝ \to G (j) \in ℝ^{*}$
21		xrltnle	$⊢ (G (j) \in ℝ^{} \land A \in ℝ^{}) \to (G (j) < A \leftrightarrow \neg A \leq G (j))$
22	20 16 21	syl2anr	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \land j \in ℝ) \to (G (j) < A \leftrightarrow \neg A \leq G (j))$
23	22	rexbidva	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (\exists j \in ℝ G (j) < A \leftrightarrow \exists j \in ℝ \neg A \leq G (j))$
24	5 18 23	3bitr4d	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (lim sup (F) < A \leftrightarrow \exists j \in ℝ G (j) < A)$

Metamath Proof Explorer

Theorem limsuplt

Proof