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

Metamath Proof Explorer

Theorem supcnvlimsupmpt

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supcnvlimsupmpt.j ⊢ Ⅎ 𝑗 𝜑
supcnvlimsupmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
supcnvlimsupmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
supcnvlimsupmpt.b ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
supcnvlimsupmpt.r ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
Assertion supcnvlimsupmpt ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) ⇝ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 supcnvlimsupmpt.j ⊢ Ⅎ 𝑗 𝜑
2 supcnvlimsupmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 supcnvlimsupmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 supcnvlimsupmpt.b ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
5 supcnvlimsupmpt.r ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
6 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑛 ) )
7 6 mpteq1d ⊢ ( 𝑘 = 𝑛 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) )
8 7 rneqd ⊢ ( 𝑘 = 𝑛 → ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) = ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) )
9 8 supeq1d ⊢ ( 𝑘 = 𝑛 → sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) , ℝ* , < ) )
10 9 cbvmptv ⊢ ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) , ℝ* , < ) )
11 3 uzssd3 ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
13 12 resmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) )
14 13 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) = ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) )
15 14 rneqd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) = ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) )
16 15 supeq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) , ℝ* , < ) = sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
17 16 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
18 10 17 eqtrid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
19 1 4 fmptd2f ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
20 2 3 19 5 supcnvlimsup ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) )
21 18 20 eqbrtrd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) ⇝ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) )