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 ⊢Ⅎ_jF
limsupmnf.a ⊢φ→A⊆ℝ
limsupmnf.f ⊢φ→F:A⟶ℝ*
Assertion limsupmnf ⊢φ→lim sup⁡F=−∞↔∀x∈ℝ∃k∈ℝ∀j∈Ak≤j→F⁡j≤x

Proof

Step Hyp Ref Expression
1 limsupmnf.j ⊢Ⅎ_jF
2 limsupmnf.a ⊢φ→A⊆ℝ
3 limsupmnf.f ⊢φ→F:A⟶ℝ*
4 eqid ⊢i∈ℝ⟼supFi+∞ℝ*<=i∈ℝ⟼supFi+∞ℝ*<
5 2 3 4 limsupmnflem ⊢φ→lim sup⁡F=−∞↔∀y∈ℝ∃i∈ℝ∀l∈Ai≤l→F⁡l≤y
6 breq2 ⊢y=x→F⁡l≤y↔F⁡l≤x
7 6 imbi2d ⊢y=x→i≤l→F⁡l≤y↔i≤l→F⁡l≤x
8 7 ralbidv ⊢y=x→∀l∈Ai≤l→F⁡l≤y↔∀l∈Ai≤l→F⁡l≤x
9 8 rexbidv ⊢y=x→∃i∈ℝ∀l∈Ai≤l→F⁡l≤y↔∃i∈ℝ∀l∈Ai≤l→F⁡l≤x
10 breq1 ⊢i=k→i≤l↔k≤l
11 10 imbi1d ⊢i=k→i≤l→F⁡l≤x↔k≤l→F⁡l≤x
12 11 ralbidv ⊢i=k→∀l∈Ai≤l→F⁡l≤x↔∀l∈Ak≤l→F⁡l≤x
13 nfv ⊢Ⅎjk≤l
14 nfcv ⊢Ⅎ_jl
15 1 14 nffv ⊢Ⅎ_jF⁡l
16 nfcv ⊢Ⅎ_j≤
17 nfcv ⊢Ⅎ_jx
18 15 16 17 nfbr ⊢ℲjF⁡l≤x
19 13 18 nfim ⊢Ⅎjk≤l→F⁡l≤x
20 nfv ⊢Ⅎlk≤j→F⁡j≤x
21 breq2 ⊢l=j→k≤l↔k≤j
22 fveq2 ⊢l=j→F⁡l=F⁡j
23 22 breq1d ⊢l=j→F⁡l≤x↔F⁡j≤x
24 21 23 imbi12d ⊢l=j→k≤l→F⁡l≤x↔k≤j→F⁡j≤x
25 19 20 24 cbvralw ⊢∀l∈Ak≤l→F⁡l≤x↔∀j∈Ak≤j→F⁡j≤x
26 25 a1i ⊢i=k→∀l∈Ak≤l→F⁡l≤x↔∀j∈Ak≤j→F⁡j≤x
27 12 26 bitrd ⊢i=k→∀l∈Ai≤l→F⁡l≤x↔∀j∈Ak≤j→F⁡j≤x
28 27 cbvrexvw ⊢∃i∈ℝ∀l∈Ai≤l→F⁡l≤x↔∃k∈ℝ∀j∈Ak≤j→F⁡j≤x
29 28 a1i ⊢y=x→∃i∈ℝ∀l∈Ai≤l→F⁡l≤x↔∃k∈ℝ∀j∈Ak≤j→F⁡j≤x
30 9 29 bitrd ⊢y=x→∃i∈ℝ∀l∈Ai≤l→F⁡l≤y↔∃k∈ℝ∀j∈Ak≤j→F⁡j≤x
31 30 cbvralvw ⊢∀y∈ℝ∃i∈ℝ∀l∈Ai≤l→F⁡l≤y↔∀x∈ℝ∃k∈ℝ∀j∈Ak≤j→F⁡j≤x
32 31 a1i ⊢φ→∀y∈ℝ∃i∈ℝ∀l∈Ai≤l→F⁡l≤y↔∀x∈ℝ∃k∈ℝ∀j∈Ak≤j→F⁡j≤x
33 5 32 bitrd ⊢φ→lim sup⁡F=−∞↔∀x∈ℝ∃k∈ℝ∀j∈Ak≤j→F⁡j≤x