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	syl5eq	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 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 ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) )