Metamath Proof Explorer


Theorem limsupmnf

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 limsupmnf.j 𝑗 𝐹
limsupmnf.a ( 𝜑𝐴 ⊆ ℝ )
limsupmnf.f ( 𝜑𝐹 : 𝐴 ⟶ ℝ* )
Assertion limsupmnf ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 limsupmnf.j 𝑗 𝐹
2 limsupmnf.a ( 𝜑𝐴 ⊆ ℝ )
3 limsupmnf.f ( 𝜑𝐹 : 𝐴 ⟶ ℝ* )
4 eqid ( 𝑖 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) , ℝ* , < ) )
5 2 3 4 limsupmnflem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ) )
6 breq2 ( 𝑦 = 𝑥 → ( ( 𝐹𝑙 ) ≤ 𝑦 ↔ ( 𝐹𝑙 ) ≤ 𝑥 ) )
7 6 imbi2d ( 𝑦 = 𝑥 → ( ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ) )
8 7 ralbidv ( 𝑦 = 𝑥 → ( ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ) )
9 8 rexbidv ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ) )
10 breq1 ( 𝑖 = 𝑘 → ( 𝑖𝑙𝑘𝑙 ) )
11 10 imbi1d ( 𝑖 = 𝑘 → ( ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ) )
12 11 ralbidv ( 𝑖 = 𝑘 → ( ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑙𝐴 ( 𝑘𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ) )
13 nfv 𝑗 𝑘𝑙
14 nfcv 𝑗 𝑙
15 1 14 nffv 𝑗 ( 𝐹𝑙 )
16 nfcv 𝑗
17 nfcv 𝑗 𝑥
18 15 16 17 nfbr 𝑗 ( 𝐹𝑙 ) ≤ 𝑥
19 13 18 nfim 𝑗 ( 𝑘𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 )
20 nfv 𝑙 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 )
21 breq2 ( 𝑙 = 𝑗 → ( 𝑘𝑙𝑘𝑗 ) )
22 fveq2 ( 𝑙 = 𝑗 → ( 𝐹𝑙 ) = ( 𝐹𝑗 ) )
23 22 breq1d ( 𝑙 = 𝑗 → ( ( 𝐹𝑙 ) ≤ 𝑥 ↔ ( 𝐹𝑗 ) ≤ 𝑥 ) )
24 21 23 imbi12d ( 𝑙 = 𝑗 → ( ( 𝑘𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
25 19 20 24 cbvralw ( ∀ 𝑙𝐴 ( 𝑘𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) )
26 25 a1i ( 𝑖 = 𝑘 → ( ∀ 𝑙𝐴 ( 𝑘𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
27 12 26 bitrd ( 𝑖 = 𝑘 → ( ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
28 27 cbvrexvw ( ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) )
29 28 a1i ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
30 9 29 bitrd ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
31 30 cbvralvw ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) )
32 31 a1i ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙𝐴 ( 𝑖𝑙 → ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
33 5 32 bitrd ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) ) )