Metamath Proof Explorer

Theorem limsupre2lem

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre2lem.1 ⊢ Ⅎ 𝑗 𝐹
limsupre2lem.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupre2lem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
Assertion limsupre2lem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre2lem.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupre2lem.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsupre2lem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 reex ⊢ ℝ ∈ V
5 4 a1i ⊢ ( 𝜑 → ℝ ∈ V )
6 5 2 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
7 3 6 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
8 7 limsupcld ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
9 xrre4 ⊢ ( ( lim sup ‘ 𝐹 ) ∈ ℝ* → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ( lim sup ‘ 𝐹 ) ≠ -∞ ∧ ( lim sup ‘ 𝐹 ) ≠ +∞ ) ) )
10 8 9 syl ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ( lim sup ‘ 𝐹 ) ≠ -∞ ∧ ( lim sup ‘ 𝐹 ) ≠ +∞ ) ) )
11 df-ne ⊢ ( ( lim sup ‘ 𝐹 ) ≠ -∞ ↔ ¬ ( lim sup ‘ 𝐹 ) = -∞ )
12 11 a1i ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≠ -∞ ↔ ¬ ( lim sup ‘ 𝐹 ) = -∞ ) )
13 1 2 3 limsupmnf ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
14 13 notbid ⊢ ( 𝜑 → ( ¬ ( lim sup ‘ 𝐹 ) = -∞ ↔ ¬ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
15 annim ⊢ ( ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ¬ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
16 15 rexbii ⊢ ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
17 rexnal ⊢ ( ∃ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ¬ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
18 16 17 bitri ⊢ ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ¬ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
19 18 ralbii ⊢ ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑘 ∈ ℝ ¬ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
20 ralnex ⊢ ( ∀ 𝑘 ∈ ℝ ¬ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ¬ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
21 19 20 bitri ⊢ ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ¬ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
22 21 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ¬ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
23 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ ¬ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
24 22 23 bitr2i ⊢ ( ¬ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
25 24 a1i ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
26 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
27 26 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
28 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ* )
29 28 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
30 27 29 xrltnled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑥 < ( 𝐹 ‘ 𝑗 ) ↔ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
31 30 bicomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
32 31 anbi2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
33 32 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
34 33 ralbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
35 34 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
36 25 35 bitrd ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
37 12 14 36 3bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≠ -∞ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
38 df-ne ⊢ ( ( lim sup ‘ 𝐹 ) ≠ +∞ ↔ ¬ ( lim sup ‘ 𝐹 ) = +∞ )
39 38 a1i ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≠ +∞ ↔ ¬ ( lim sup ‘ 𝐹 ) = +∞ ) )
40 1 2 3 limsuppnf ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
41 40 notbid ⊢ ( 𝜑 → ( ¬ ( lim sup ‘ 𝐹 ) = +∞ ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
42 29 27 xrltnled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
43 42 imbi2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
44 43 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
45 44 rexbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
46 45 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
47 imnan ⊢ ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
48 47 ralbii ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
49 ralnex ⊢ ( ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
50 48 49 bitri ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
51 50 rexbii ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
52 rexnal ⊢ ( ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
53 51 52 bitri ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
54 53 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
55 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
56 54 55 bitri ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
57 56 a1i ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
58 46 57 bitr2d ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
59 39 41 58 3bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≠ +∞ ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
60 37 59 anbi12d ⊢ ( 𝜑 → ( ( ( lim sup ‘ 𝐹 ) ≠ -∞ ∧ ( lim sup ‘ 𝐹 ) ≠ +∞ ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) ) )
61 10 60 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) ) )