Metamath Proof Explorer

Theorem 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 ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
Assertion limsuplt ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → lim sup ⁡ F < A ↔ ∃ j ∈ ℝ G ⁡ j < A

Proof

Step Hyp Ref Expression
1 limsupval.1 ⊢ G = k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
2 1 limsuple ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ≤ lim sup ⁡ F ↔ ∀ j ∈ ℝ A ≤ G ⁡ j
3 2 notbid ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → ¬ A ≤ lim sup ⁡ F ↔ ¬ ∀ j ∈ ℝ A ≤ G ⁡ j
4 rexnal ⊢ ∃ j ∈ ℝ ¬ A ≤ G ⁡ j ↔ ¬ ∀ j ∈ ℝ A ≤ G ⁡ j
5 3 4 bitr4di ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → ¬ A ≤ lim sup ⁡ F ↔ ∃ j ∈ ℝ ¬ A ≤ G ⁡ j
6 simp2 ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → F : B ⟶ ℝ *
7 reex ⊢ ℝ ∈ V
8 7 ssex ⊢ B ⊆ ℝ → B ∈ V
9 8 3ad2ant1 ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → B ∈ V
10 xrex ⊢ ℝ * ∈ V
11 10 a1i ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → ℝ * ∈ V
12 fex2 ⊢ F : B ⟶ ℝ * ∧ B ∈ V ∧ ℝ * ∈ V → F ∈ V
13 6 9 11 12 syl3anc ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → F ∈ V
14 limsupcl ⊢ F ∈ V → lim sup ⁡ F ∈ ℝ *
15 13 14 syl ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → lim sup ⁡ F ∈ ℝ *
16 simp3 ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ∈ ℝ *
17 xrltnle ⊢ lim sup ⁡ F ∈ ℝ * ∧ A ∈ ℝ * → lim sup ⁡ F < A ↔ ¬ A ≤ lim sup ⁡ F
18 15 16 17 syl2anc ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → lim sup ⁡ F < A ↔ ¬ A ≤ lim sup ⁡ F
19 1 limsupgf ⊢ G : ℝ ⟶ ℝ *
20 19 ffvelrni ⊢ j ∈ ℝ → G ⁡ j ∈ ℝ *
21 xrltnle ⊢ G ⁡ j ∈ ℝ * ∧ A ∈ ℝ * → G ⁡ j < A ↔ ¬ A ≤ G ⁡ j
22 20 16 21 syl2anr ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * ∧ j ∈ ℝ → G ⁡ j < A ↔ ¬ A ≤ G ⁡ j
23 22 rexbidva ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → ∃ j ∈ ℝ G ⁡ j < A ↔ ∃ j ∈ ℝ ¬ A ≤ G ⁡ j
24 5 18 23 3bitr4d ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → lim sup ⁡ F < A ↔ ∃ j ∈ ℝ G ⁡ j < A