limsuple

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	limsuple	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq lim sup (F) \leftrightarrow \forall j \in ℝ A \leq G (j))$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		simp2	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to F : B ⟶ ℝ^{*}$
3		reex	$⊢ ℝ \in V$
4	3	ssex	$⊢ B \subseteq ℝ \to B \in V$
5	4	3ad2ant1	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to B \in V$
6		xrex	$⊢ ℝ^{*} \in V$
7	6	a1i	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to ℝ^{*} \in V$
8		fex2	$⊢ (F : B ⟶ ℝ^{} \land B \in V \land ℝ^{} \in V) \to F \in V$
9	2 5 7 8	syl3anc	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to F \in V$
10	1	limsupval	$⊢ F \in V \to lim sup (F) = sup (ran G ℝ^{*} <)$
11	9 10	syl	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to lim sup (F) = sup (ran G ℝ^{*} <)$
12	11	breq2d	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq lim sup (F) \leftrightarrow A \leq sup (ran G ℝ^{*} <))$
13	1	limsupgf	$⊢ G : ℝ ⟶ ℝ^{*}$
14		frn	$⊢ G : ℝ ⟶ ℝ^{} \to ran G \subseteq ℝ^{}$
15	13 14	ax-mp	$⊢ ran G \subseteq ℝ^{*}$
16		simp3	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to A \in ℝ^{*}$
17		infxrgelb	$⊢ (ran G \subseteq ℝ^{} \land A \in ℝ^{}) \to (A \leq sup (ran G ℝ^{*} <) \leftrightarrow \forall x \in ran G A \leq x)$
18	15 16 17	sylancr	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq sup (ran G ℝ^{*} <) \leftrightarrow \forall x \in ran G A \leq x)$
19		ffn	$⊢ G : ℝ ⟶ ℝ^{*} \to G Fn ℝ$
20	13 19	ax-mp	$⊢ G Fn ℝ$
21		breq2	$⊢ x = G (j) \to (A \leq x \leftrightarrow A \leq G (j))$
22	21	ralrn	$⊢ G Fn ℝ \to (\forall x \in ran G A \leq x \leftrightarrow \forall j \in ℝ A \leq G (j))$
23	20 22	ax-mp	$⊢ \forall x \in ran G A \leq x \leftrightarrow \forall j \in ℝ A \leq G (j)$
24	18 23	bitrdi	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq sup (ran G ℝ^{*} <) \leftrightarrow \forall j \in ℝ A \leq G (j))$
25	12 24	bitrd	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq lim sup (F) \leftrightarrow \forall j \in ℝ A \leq G (j))$

Metamath Proof Explorer

Theorem limsuple

Proof