Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 limsupval.1 ⊢ G = k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
2 simp2 ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → F : B ⟶ ℝ *
3 reex ⊢ ℝ ∈ V
4 3 ssex ⊢ B ⊆ ℝ → B ∈ V
5 4 3ad2ant1 ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → B ∈ V
6 xrex ⊢ ℝ * ∈ V
7 6 a1i ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → ℝ * ∈ V
8 fex2 ⊢ F : B ⟶ ℝ * ∧ B ∈ V ∧ ℝ * ∈ V → F ∈ V
9 2 5 7 8 syl3anc ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → F ∈ V
10 1 limsupval ⊢ F ∈ V → lim sup ⁡ F = sup ran ⁡ G ℝ * <
11 9 10 syl ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → lim sup ⁡ F = sup ran ⁡ G ℝ * <
12 11 breq2d ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ≤ lim sup ⁡ F ↔ A ≤ sup ran ⁡ G ℝ * <
13 1 limsupgf ⊢ G : ℝ ⟶ ℝ *
14 frn ⊢ G : ℝ ⟶ ℝ * → ran ⁡ G ⊆ ℝ *
15 13 14 ax-mp ⊢ ran ⁡ G ⊆ ℝ *
16 simp3 ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ∈ ℝ *
17 infxrgelb ⊢ ran ⁡ G ⊆ ℝ * ∧ A ∈ ℝ * → A ≤ sup ran ⁡ G ℝ * < ↔ ∀ x ∈ ran ⁡ G A ≤ x
18 15 16 17 sylancr ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ≤ sup ran ⁡ G ℝ * < ↔ ∀ x ∈ ran ⁡ G A ≤ x
19 ffn ⊢ G : ℝ ⟶ ℝ * → G Fn ℝ
20 13 19 ax-mp ⊢ G Fn ℝ
21 breq2 ⊢ x = G ⁡ j → A ≤ x ↔ A ≤ G ⁡ j
22 21 ralrn ⊢ G Fn ℝ → ∀ x ∈ ran ⁡ G A ≤ x ↔ ∀ j ∈ ℝ A ≤ G ⁡ j
23 20 22 ax-mp ⊢ ∀ x ∈ ran ⁡ G A ≤ x ↔ ∀ j ∈ ℝ A ≤ G ⁡ j
24 18 23 bitrdi ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ≤ sup ran ⁡ G ℝ * < ↔ ∀ j ∈ ℝ A ≤ G ⁡ j
25 12 24 bitrd ⊢ B ⊆ ℝ ∧ F : B ⟶ ℝ * ∧ A ∈ ℝ * → A ≤ lim sup ⁡ F ↔ ∀ j ∈ ℝ A ≤ G ⁡ j