Metamath Proof Explorer

Theorem limsupmnflem

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupmnflem.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupmnflem.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
limsupmnflem.g ⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
Assertion limsupmnflem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 limsupmnflem.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 limsupmnflem.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
3 limsupmnflem.g ⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
4 nfv ⊢ Ⅎ 𝑘 𝜑
5 reex ⊢ ℝ ∈ V
6 5 a1i ⊢ ( 𝜑 → ℝ ∈ V )
7 6 1 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
8 4 7 2 3 limsupval3 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
9 3 rneqi ⊢ ran 𝐺 = ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
10 9 infeq1i ⊢ inf ( ran 𝐺 , ℝ* , < ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < )
11 10 a1i ⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ* , < ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) )
12 8 11 eqtrd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) )
13 12 eqeq1d ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) = -∞ ) )
14 nfv ⊢ Ⅎ 𝑥 𝜑
15 2 fimassd ⊢ ( 𝜑 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ* )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ* )
17 16 supxrcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ∈ ℝ* )
18 4 14 17 infxrunb3rnmpt ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) = -∞ ) )
19 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ* )
20 ressxr ⊢ ℝ ⊆ ℝ*
21 20 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
22 21 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ* )
23 supxrleub ⊢ ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) )
24 19 22 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) )
26 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
27 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝐹 Fn 𝐴 )
28 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ 𝐴 )
29 20 sseli ⊢ ( 𝑘 ∈ ℝ → 𝑘 ∈ ℝ* )
30 29 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ∈ ℝ* )
31 pnfxr ⊢ +∞ ∈ ℝ*
32 31 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → +∞ ∈ ℝ* )
33 20 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ℝ ⊆ ℝ* )
34 1 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℝ )
35 33 34 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℝ* )
36 35 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ℝ* )
37 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ≤ 𝑗 )
38 34 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 < +∞ )
39 38 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 < +∞ )
40 30 32 36 37 39 elicod ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ( 𝑘 [,) +∞ ) )
41 27 28 40 fnfvimad ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
42 41 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
43 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 )
44 breq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑗 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
45 44 rspcva ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
46 42 43 45 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
47 46 adantl4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
48 47 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
49 48 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
50 49 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 → ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
51 nfcv ⊢ Ⅎ 𝑗 𝐹
52 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → 𝐹 Fn 𝐴 )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
54 51 52 53 fvelimad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) = 𝑦 )
55 54 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) = 𝑦 )
56 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ ℝ )
57 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
58 56 57 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
59 nfv ⊢ Ⅎ 𝑗 𝑦 ≤ 𝑥
60 29 adantr ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑘 ∈ ℝ* )
61 31 a1i ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → +∞ ∈ ℝ* )
62 elinel2 ⊢ ( 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → 𝑗 ∈ ( 𝑘 [,) +∞ ) )
63 62 adantl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑗 ∈ ( 𝑘 [,) +∞ ) )
64 60 61 63 icogelbd ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑘 ≤ 𝑗 )
65 64 adantlr ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑘 ≤ 𝑗 )
66 elinel1 ⊢ ( 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → 𝑗 ∈ 𝐴 )
67 66 adantl ⊢ ( ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑗 ∈ 𝐴 )
68 rspa ⊢ ( ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
69 67 68 syldan ⊢ ( ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
70 69 adantll ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
71 65 70 mpd ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
72 id ⊢ ( ( 𝐹 ‘ 𝑗 ) = 𝑦 → ( 𝐹 ‘ 𝑗 ) = 𝑦 )
73 72 eqcomd ⊢ ( ( 𝐹 ‘ 𝑗 ) = 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑗 ) )
74 73 adantl ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ( 𝐹 ‘ 𝑗 ) = 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑗 ) )
75 simpl ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ( 𝐹 ‘ 𝑗 ) = 𝑦 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
76 74 75 eqbrtrd ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ( 𝐹 ‘ 𝑗 ) = 𝑦 ) → 𝑦 ≤ 𝑥 )
77 76 ex ⊢ ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ( ( 𝐹 ‘ 𝑗 ) = 𝑦 → 𝑦 ≤ 𝑥 ) )
78 71 77 syl ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( ( 𝐹 ‘ 𝑗 ) = 𝑦 → 𝑦 ≤ 𝑥 ) )
79 78 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( ( 𝐹 ‘ 𝑗 ) = 𝑦 → 𝑦 ≤ 𝑥 ) )
80 79 ex ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → ( ( 𝐹 ‘ 𝑗 ) = 𝑦 → 𝑦 ≤ 𝑥 ) ) )
81 58 59 80 rexlimd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( ∃ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) = 𝑦 → 𝑦 ≤ 𝑥 ) )
82 81 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ ∃ 𝑗 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) = 𝑦 ) → 𝑦 ≤ 𝑥 )
83 55 82 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ≤ 𝑥 )
84 83 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 )
85 84 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 )
86 24 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) )
87 85 86 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 )
88 87 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ) )
89 88 25 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ) )
90 50 89 impbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) 𝑦 ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
91 25 90 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
92 91 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
93 92 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
94 13 18 93 3bitr2d ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )