Proof of Theorem limsuppnflem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . . . . 7
⊢ (𝜑 → 𝜑) | 
| 2 |  | imnan 399 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 3 | 2 | ralbii 3093 | . . . . . . . . . . . . 13
⊢
(∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ∀𝑗 ∈ 𝐴 ¬ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 4 |  | ralnex 3072 | . . . . . . . . . . . . 13
⊢
(∀𝑗 ∈
𝐴 ¬ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 5 | 3, 4 | bitri 275 | . . . . . . . . . . . 12
⊢
(∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 6 | 5 | rexbii 3094 | . . . . . . . . . . 11
⊢
(∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ∃𝑘 ∈ ℝ ¬ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 7 |  | rexnal 3100 | . . . . . . . . . . 11
⊢
(∃𝑘 ∈
ℝ ¬ ∃𝑗
∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 8 | 6, 7 | bitri 275 | . . . . . . . . . 10
⊢
(∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 9 | 8 | rexbii 3094 | . . . . . . . . 9
⊢
(∃𝑥 ∈
ℝ ∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ∃𝑥 ∈ ℝ ¬ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 10 |  | rexnal 3100 | . . . . . . . . 9
⊢
(∃𝑥 ∈
ℝ ¬ ∀𝑘
∈ ℝ ∃𝑗
∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 11 | 9, 10 | bitri 275 | . . . . . . . 8
⊢
(∃𝑥 ∈
ℝ ∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 12 | 11 | biimpri 228 | . . . . . . 7
⊢ (¬
∀𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗))) | 
| 13 |  | simp1 1137 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ∧ 𝑘 ≤ 𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴)) | 
| 14 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗))) | 
| 15 | 14 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ∧ 𝑘 ≤ 𝑗) → ¬ 𝑥 ≤ (𝐹‘𝑗)) | 
| 16 | 15 | 3adant1 1131 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ∧ 𝑘 ≤ 𝑗) → ¬ 𝑥 ≤ (𝐹‘𝑗)) | 
| 17 |  | limsuppnflem.f | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | 
| 18 | 17 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐹‘𝑗) ∈
ℝ*) | 
| 19 | 18 | ad4ant14 752 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → (𝐹‘𝑗) ∈
ℝ*) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ∈
ℝ*) | 
| 21 |  | simpllr 776 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → 𝑥 ∈ ℝ) | 
| 22 |  | rexr 11307 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → 𝑥 ∈ ℝ*) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ*) | 
| 25 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → ¬ 𝑥 ≤ (𝐹‘𝑗)) | 
| 26 | 18 | ad4ant13 751 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ∈
ℝ*) | 
| 27 | 22 | ad3antlr 731 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ*) | 
| 28 | 26, 27 | xrltnled 45374 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → ((𝐹‘𝑗) < 𝑥 ↔ ¬ 𝑥 ≤ (𝐹‘𝑗))) | 
| 29 | 25, 28 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) < 𝑥) | 
| 30 | 29 | adantllr 719 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) < 𝑥) | 
| 31 | 20, 24, 30 | xrltled 13192 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ≤ 𝑥) | 
| 32 | 13, 16, 31 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑥) | 
| 33 | 32 | 3exp 1120 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → ((𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) → (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) | 
| 34 | 33 | ralimdva 3167 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) → (∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) → ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) | 
| 35 | 34 | reximdva 3168 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) | 
| 36 | 35 | reximdva 3168 | . . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗)) → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) | 
| 37 | 36 | imp 406 | . . . . . . 7
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ (𝐹‘𝑗))) → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) | 
| 38 | 1, 12, 37 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) | 
| 39 |  | reex 11246 | . . . . . . . . . . . . . 14
⊢ ℝ
∈ V | 
| 40 | 39 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) | 
| 41 |  | limsuppnflem.a | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 42 | 40, 41 | ssexd 5324 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ V) | 
| 43 | 17, 42 | fexd 7247 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) | 
| 44 | 43 | limsupcld 45705 | . . . . . . . . . 10
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ*) | 
| 45 | 44 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → (lim sup‘𝐹) ∈
ℝ*) | 
| 46 | 22 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → 𝑥 ∈ ℝ*) | 
| 47 |  | pnfxr 11315 | . . . . . . . . . 10
⊢ +∞
∈ ℝ* | 
| 48 | 47 | a1i 11 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → +∞ ∈
ℝ*) | 
| 49 |  | limsuppnflem.j | . . . . . . . . . 10
⊢
Ⅎ𝑗𝐹 | 
| 50 | 41 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → 𝐴 ⊆ ℝ) | 
| 51 | 17 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → 𝐹:𝐴⟶ℝ*) | 
| 52 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) | 
| 53 | 49, 50, 51, 46, 52 | limsupbnd1f 45701 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → (lim sup‘𝐹) ≤ 𝑥) | 
| 54 |  | ltpnf 13162 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) | 
| 55 | 54 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → 𝑥 < +∞) | 
| 56 | 45, 46, 48, 53, 55 | xrlelttrd 13202 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → (lim sup‘𝐹) < +∞) | 
| 57 | 56 | rexlimdva2 3157 | . . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) → (lim sup‘𝐹) < +∞)) | 
| 58 | 57 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → (lim sup‘𝐹) < +∞) | 
| 59 | 38, 58 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → (lim sup‘𝐹) < +∞) | 
| 60 | 59 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ (lim sup‘𝐹) = +∞) ∧ ¬
∀𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → (lim sup‘𝐹) < +∞) | 
| 61 |  | id 22 | . . . . . . . 8
⊢ ((lim
sup‘𝐹) = +∞
→ (lim sup‘𝐹) =
+∞) | 
| 62 | 47 | a1i 11 | . . . . . . . 8
⊢ ((lim
sup‘𝐹) = +∞
→ +∞ ∈ ℝ*) | 
| 63 | 61, 62 | eqeltrd 2841 | . . . . . . 7
⊢ ((lim
sup‘𝐹) = +∞
→ (lim sup‘𝐹)
∈ ℝ*) | 
| 64 | 63, 61 | xreqnltd 45406 | . . . . . 6
⊢ ((lim
sup‘𝐹) = +∞
→ ¬ (lim sup‘𝐹) < +∞) | 
| 65 | 64 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ (lim sup‘𝐹) = +∞) → ¬ (lim
sup‘𝐹) <
+∞) | 
| 66 | 65 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (lim sup‘𝐹) = +∞) ∧ ¬
∀𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → ¬ (lim sup‘𝐹) <
+∞) | 
| 67 | 60, 66 | condan 818 | . . 3
⊢ ((𝜑 ∧ (lim sup‘𝐹) = +∞) →
∀𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 68 | 67 | ex 412 | . 2
⊢ (𝜑 → ((lim sup‘𝐹) = +∞ →
∀𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) | 
| 69 | 41 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → 𝐴 ⊆ ℝ) | 
| 70 | 17 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → 𝐹:𝐴⟶ℝ*) | 
| 71 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) | 
| 72 | 49, 69, 70, 71 | limsuppnfd 45717 | . . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) → (lim sup‘𝐹) = +∞) | 
| 73 | 72 | ex 412 | . 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) → (lim sup‘𝐹) = +∞)) | 
| 74 | 68, 73 | impbid 212 | 1
⊢ (𝜑 → ((lim sup‘𝐹) = +∞ ↔
∀𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |