This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsuppnflem

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsuppnflem.j ⊢ Ⅎ 𝑗 𝐹
limsuppnflem.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsuppnflem.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
Assertion limsuppnflem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )

Proof

Step Hyp Ref Expression
1 limsuppnflem.j ⊢ Ⅎ 𝑗 𝐹
2 limsuppnflem.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsuppnflem.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 id ⊢ ( 𝜑 → 𝜑 )
5 imnan ⊢ ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
6 5 ralbii ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
7 ralnex ⊢ ( ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
8 6 7 bitri ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
9 8 rexbii ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
10 rexnal ⊢ ( ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
11 9 10 bitri ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
12 11 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
13 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
14 12 13 bitri ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
15 14 biimpri ⊢ ( ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
16 simp1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ≤ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) )
17 id ⊢ ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
18 17 imp ⊢ ( ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ≤ 𝑗 ) → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
19 18 3adant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ≤ 𝑗 ) → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
20 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
21 20 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
22 21 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
23 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
24 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
25 23 24 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
26 25 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* )
27 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
28 20 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
29 24 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* )
30 28 29 xrltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑗 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
31 27 30 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) < 𝑥 )
32 31 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) < 𝑥 )
33 22 26 32 xrltled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
34 16 19 33 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
35 34 3exp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
36 35 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
37 36 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
38 37 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
39 38 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
40 4 15 39 syl2an ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
41 reex ⊢ ℝ ∈ V
42 41 a1i ⊢ ( 𝜑 → ℝ ∈ V )
43 42 2 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
44 3 43 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
45 44 limsupcld ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
47 24 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → 𝑥 ∈ ℝ* )
48 pnfxr ⊢ +∞ ∈ ℝ*
49 48 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → +∞ ∈ ℝ* )
50 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → 𝐴 ⊆ ℝ )
51 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
52 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
53 1 50 51 47 52 limsupbnd1f ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( lim sup ‘ 𝐹 ) ≤ 𝑥 )
54 ltpnf ⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
55 54 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → 𝑥 < +∞ )
56 46 47 49 53 55 xrlelttrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( lim sup ‘ 𝐹 ) < +∞ )
57 56 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( lim sup ‘ 𝐹 ) < +∞ ) )
58 57 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( lim sup ‘ 𝐹 ) < +∞ )
59 40 58 syldan ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( lim sup ‘ 𝐹 ) < +∞ )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = +∞ ) ∧ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( lim sup ‘ 𝐹 ) < +∞ )
61 id ⊢ ( ( lim sup ‘ 𝐹 ) = +∞ → ( lim sup ‘ 𝐹 ) = +∞ )
62 48 a1i ⊢ ( ( lim sup ‘ 𝐹 ) = +∞ → +∞ ∈ ℝ* )
63 61 62 eqeltrd ⊢ ( ( lim sup ‘ 𝐹 ) = +∞ → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
64 63 61 xreqnltd ⊢ ( ( lim sup ‘ 𝐹 ) = +∞ → ¬ ( lim sup ‘ 𝐹 ) < +∞ )
65 64 adantl ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = +∞ ) → ¬ ( lim sup ‘ 𝐹 ) < +∞ )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = +∞ ) ∧ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ¬ ( lim sup ‘ 𝐹 ) < +∞ )
67 60 66 condan ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = +∞ ) → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
68 67 ex ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = +∞ → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
69 2 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝐴 ⊆ ℝ )
70 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
71 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
72 1 69 70 71 limsuppnfd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( lim sup ‘ 𝐹 ) = +∞ )
73 72 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( lim sup ‘ 𝐹 ) = +∞ ) )
74 68 73 impbid ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )