Metamath Proof Explorer

Theorem limsupub2

Description: A extended real valued function, with limsup that is not +oo , is eventually less than +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses limsupub2.1 ⊢ Ⅎ 𝑗 𝜑
limsupub2.2 ⊢ Ⅎ 𝑗 𝐹
limsupub2.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupub2.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
limsupub2.5 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
Assertion limsupub2 ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) )

Proof

Step Hyp Ref Expression
1 limsupub2.1 ⊢ Ⅎ 𝑗 𝜑
2 limsupub2.2 ⊢ Ⅎ 𝑗 𝐹
3 limsupub2.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 limsupub2.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
5 limsupub2.5 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
6 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ ℝ
7 1 6 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ ℝ )
8 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ ℝ
9 7 8 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ )
10 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
11 10 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
12 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
13 12 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
14 pnfxr ⊢ +∞ ∈ ℝ*
15 14 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → +∞ ∈ ℝ* )
16 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
17 ltpnf ⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
18 17 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝑥 < +∞ )
19 11 13 15 16 18 xrlelttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) < +∞ )
20 19 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑗 ) < +∞ ) )
21 20 imim2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) ) )
22 9 21 ralimdaa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) ) )
23 22 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) ) )
24 23 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) )
25 1 2 3 4 5 limsupub ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
26 24 25 r19.29a ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) )