Metamath Proof Explorer


Theorem limsuppnfd

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsuppnfd.j 𝑗 𝐹
limsuppnfd.a ( 𝜑𝐴 ⊆ ℝ )
limsuppnfd.f ( 𝜑𝐹 : 𝐴 ⟶ ℝ* )
limsuppnfd.u ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) )
Assertion limsuppnfd ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ )

Proof

Step Hyp Ref Expression
1 limsuppnfd.j 𝑗 𝐹
2 limsuppnfd.a ( 𝜑𝐴 ⊆ ℝ )
3 limsuppnfd.f ( 𝜑𝐹 : 𝐴 ⟶ ℝ* )
4 limsuppnfd.u ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) )
5 breq1 ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹𝑗 ) ↔ 𝑦 ≤ ( 𝐹𝑗 ) ) )
6 5 anbi2d ( 𝑥 = 𝑦 → ( ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ↔ ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
7 6 rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ↔ ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
8 breq1 ( 𝑘 = 𝑖 → ( 𝑘𝑗𝑖𝑗 ) )
9 8 anbi1d ( 𝑘 = 𝑖 → ( ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ↔ ( 𝑖𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
10 9 rexbidv ( 𝑘 = 𝑖 → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ↔ ∃ 𝑗𝐴 ( 𝑖𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ) )
11 nfv 𝑙 ( 𝑖𝑗𝑦 ≤ ( 𝐹𝑗 ) )
12 nfv 𝑗 𝑖𝑙
13 nfcv 𝑗 𝑦
14 nfcv 𝑗
15 nfcv 𝑗 𝑙
16 1 15 nffv 𝑗 ( 𝐹𝑙 )
17 13 14 16 nfbr 𝑗 𝑦 ≤ ( 𝐹𝑙 )
18 12 17 nfan 𝑗 ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) )
19 breq2 ( 𝑗 = 𝑙 → ( 𝑖𝑗𝑖𝑙 ) )
20 fveq2 ( 𝑗 = 𝑙 → ( 𝐹𝑗 ) = ( 𝐹𝑙 ) )
21 20 breq2d ( 𝑗 = 𝑙 → ( 𝑦 ≤ ( 𝐹𝑗 ) ↔ 𝑦 ≤ ( 𝐹𝑙 ) ) )
22 19 21 anbi12d ( 𝑗 = 𝑙 → ( ( 𝑖𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ↔ ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) ) ) )
23 11 18 22 cbvrexw ( ∃ 𝑗𝐴 ( 𝑖𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ↔ ∃ 𝑙𝐴 ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) ) )
24 23 a1i ( 𝑘 = 𝑖 → ( ∃ 𝑗𝐴 ( 𝑖𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ↔ ∃ 𝑙𝐴 ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) ) ) )
25 10 24 bitrd ( 𝑘 = 𝑖 → ( ∃ 𝑗𝐴 ( 𝑘𝑗𝑦 ≤ ( 𝐹𝑗 ) ) ↔ ∃ 𝑙𝐴 ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) ) ) )
26 7 25 cbvral2vw ( ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗𝐴 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ↔ ∀ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙𝐴 ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) ) )
27 4 26 sylib ( 𝜑 → ∀ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙𝐴 ( 𝑖𝑙𝑦 ≤ ( 𝐹𝑙 ) ) )
28 eqid ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
29 2 3 27 28 limsuppnfdlem ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ )