Metamath Proof Explorer


Theorem limsupre3lem

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 less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsupre3lem.1 𝑗 𝐹
2 limsupre3lem.2 ( 𝜑𝐴 ⊆ ℝ )
3 limsupre3lem.3 ( 𝜑𝐹 : 𝐴 ⟶ ℝ* )
4 1 2 3 limsupre2 ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ) ) )
5 simp2 ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) → 𝑦 ∈ ℝ )
6 nfv 𝑗 ( 𝜑𝑦 ∈ ℝ )
7 simp3l ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) → 𝑘𝑗 )
8 simp1r ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴𝑦 < ( 𝐹𝑗 ) ) → 𝑦 ∈ ℝ )
9 8 rexrd ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴𝑦 < ( 𝐹𝑗 ) ) → 𝑦 ∈ ℝ* )
10 3 ffvelrnda ( ( 𝜑𝑗𝐴 ) → ( 𝐹𝑗 ) ∈ ℝ* )
11 10 adantlr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) → ( 𝐹𝑗 ) ∈ ℝ* )
12 11 3adant3 ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴𝑦 < ( 𝐹𝑗 ) ) → ( 𝐹𝑗 ) ∈ ℝ* )
13 simp3 ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴𝑦 < ( 𝐹𝑗 ) ) → 𝑦 < ( 𝐹𝑗 ) )
14 9 12 13 xrltled ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴𝑦 < ( 𝐹𝑗 ) ) → 𝑦 ≤ ( 𝐹𝑗 ) )
15 14 3adant3l ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) → 𝑦 ≤ ( 𝐹𝑗 ) )
16 7 15 jca ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) → ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) )
17 16 3exp ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑗𝐴 → ( ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) → ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) ) )
18 6 17 reximdai ( ( 𝜑𝑦 ∈ ℝ ) → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) → ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
19 18 ralimdv ( ( 𝜑𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
20 19 3impia ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) )
21 breq1 ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹𝑗 ) ↔ 𝑦 ≤ ( 𝐹𝑗 ) ) )
22 21 anbi2d ( 𝑥 = 𝑦 → ( ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ↔ ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
23 22 rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ↔ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
24 23 ralbidv ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
25 24 rspcev ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) )
26 5 20 25 syl2anc ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) )
27 26 3exp ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) ) )
28 27 rexlimdv ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) )
29 peano2rem ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ )
30 29 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ( 𝑥 − 1 ) ∈ ℝ )
31 nfv 𝑗 ( 𝜑𝑥 ∈ ℝ )
32 simp3l ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → 𝑘𝑗 )
33 simp1r ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → 𝑥 ∈ ℝ )
34 29 rexrd ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ* )
35 33 34 syl ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ( 𝑥 − 1 ) ∈ ℝ* )
36 33 rexrd ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → 𝑥 ∈ ℝ* )
37 10 adantlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) → ( 𝐹𝑗 ) ∈ ℝ* )
38 37 3adant3 ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ( 𝐹𝑗 ) ∈ ℝ* )
39 33 ltm1d ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ( 𝑥 − 1 ) < 𝑥 )
40 simp3r ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → 𝑥 ≤ ( 𝐹𝑗 ) )
41 35 36 38 39 40 xrltletrd ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ( 𝑥 − 1 ) < ( 𝐹𝑗 ) )
42 32 41 jca ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ∧ ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) )
43 42 3exp ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑗𝐴 → ( ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) → ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) ) )
44 31 43 reximdai ( ( 𝜑𝑥 ∈ ℝ ) → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) → ∃ 𝑗𝐴 ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) )
45 44 ralimdv ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) )
46 45 imp ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) )
47 breq1 ( 𝑦 = ( 𝑥 − 1 ) → ( 𝑦 < ( 𝐹𝑗 ) ↔ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) )
48 47 anbi2d ( 𝑦 = ( 𝑥 − 1 ) → ( ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ↔ ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) )
49 48 rexbidv ( 𝑦 = ( 𝑥 − 1 ) → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ↔ ∃ 𝑗𝐴 ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) )
50 49 ralbidv ( 𝑦 = ( 𝑥 − 1 ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) )
51 50 rspcev ( ( ( 𝑥 − 1 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹𝑗 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) )
52 30 46 51 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) )
53 52 rexlimdva2 ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ) )
54 28 53 impbid ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ) )
55 simplr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ) → 𝑦 ∈ ℝ )
56 11 adantr ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) < 𝑦 ) → ( 𝐹𝑗 ) ∈ ℝ* )
57 rexr ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
58 57 ad3antlr ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) < 𝑦 ) → 𝑦 ∈ ℝ* )
59 simpr ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) < 𝑦 ) → ( 𝐹𝑗 ) < 𝑦 )
60 56 58 59 xrltled ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) < 𝑦 ) → ( 𝐹𝑗 ) ≤ 𝑦 )
61 60 ex ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) → ( ( 𝐹𝑗 ) < 𝑦 → ( 𝐹𝑗 ) ≤ 𝑦 ) )
62 61 imim2d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝐴 ) → ( ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) → ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
63 62 ralimdva ( ( 𝜑𝑦 ∈ ℝ ) → ( ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) → ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
64 63 reximdv ( ( 𝜑𝑦 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
65 64 imp ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) )
66 breq2 ( 𝑥 = 𝑦 → ( ( 𝐹𝑗 ) ≤ 𝑥 ↔ ( 𝐹𝑗 ) ≤ 𝑦 ) )
67 66 imbi2d ( 𝑥 = 𝑦 → ( ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ↔ ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
68 67 ralbidv ( 𝑥 = 𝑦 → ( ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
69 68 rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
70 69 rspcev ( ( 𝑦 ∈ ℝ ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) )
71 55 65 70 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) )
72 71 rexlimdva2 ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
73 peano2re ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
74 73 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) → ( 𝑥 + 1 ) ∈ ℝ )
75 37 adantr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) ≤ 𝑥 ) → ( 𝐹𝑗 ) ∈ ℝ* )
76 rexr ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
77 76 ad3antlr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
78 73 rexrd ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ* )
79 78 ad3antlr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) ≤ 𝑥 ) → ( 𝑥 + 1 ) ∈ ℝ* )
80 simpr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) ≤ 𝑥 ) → ( 𝐹𝑗 ) ≤ 𝑥 )
81 ltp1 ( 𝑥 ∈ ℝ → 𝑥 < ( 𝑥 + 1 ) )
82 81 ad3antlr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) ≤ 𝑥 ) → 𝑥 < ( 𝑥 + 1 ) )
83 75 77 79 80 82 xrlelttrd ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) ∧ ( 𝐹𝑗 ) ≤ 𝑥 ) → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) )
84 83 ex ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) → ( ( 𝐹𝑗 ) ≤ 𝑥 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) )
85 84 imim2d ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝐴 ) → ( ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) → ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) )
86 85 ralimdva ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) → ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) )
87 86 reximdv ( ( 𝜑𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) )
88 87 imp ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) )
89 breq2 ( 𝑦 = ( 𝑥 + 1 ) → ( ( 𝐹𝑗 ) < 𝑦 ↔ ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) )
90 89 imbi2d ( 𝑦 = ( 𝑥 + 1 ) → ( ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ↔ ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) )
91 90 ralbidv ( 𝑦 = ( 𝑥 + 1 ) → ( ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ↔ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) )
92 91 rexbidv ( 𝑦 = ( 𝑥 + 1 ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) )
93 92 rspcev ( ( ( 𝑥 + 1 ) ∈ ℝ ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < ( 𝑥 + 1 ) ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) )
94 74 88 93 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) )
95 94 rexlimdva2 ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ) )
96 72 95 impbid ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
97 54 96 anbi12d ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 < ( 𝐹𝑗 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) < 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) ) )
98 4 97 bitrd ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) ) )