This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupubuzmpt

Description: If the limsup is not +oo , then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupubuzmpt.j ⊢ Ⅎ 𝑗 𝜑
limsupubuzmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupubuzmpt.b ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
limsupubuzmpt.n ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ≠ +∞ )
Assertion limsupubuzmpt ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 limsupubuzmpt.j ⊢ Ⅎ 𝑗 𝜑
2 limsupubuzmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 limsupubuzmpt.b ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
4 limsupubuzmpt.n ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ≠ +∞ )
5 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ 𝐵 )
6 eqid ⊢ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑗 ∈ 𝑍 ↦ 𝐵 )
7 1 3 6 fmptdf ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
8 5 2 7 4 limsupubuz ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 )
9 6 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) )
10 9 3 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) = 𝐵 )
11 10 breq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
12 1 11 ralbida ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
13 12 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
14 8 13 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 )
15 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑥 ) )
16 15 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
17 16 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )
18 14 17 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )