Theorem limsupvaluzmpt

Description: The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo ). (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsupvaluzmpt.j	⊢ Ⅎ 𝑗 𝜑
2		limsupvaluzmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupvaluzmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		limsupvaluzmpt.b	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
5	1 4	fmptd2f	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* )
6	2 3 5	limsupvaluz	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )
7	3	uzssd3	⊢ ( 𝑘 ∈ 𝑍 → ( ℤ≥ ‘ 𝑘 ) ⊆ 𝑍 )
8	7	resmptd	⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) )
9	8	rneqd	⊢ ( 𝑘 ∈ 𝑍 → ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) )
10	9	supeq1d	⊢ ( 𝑘 ∈ 𝑍 → sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) = sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) )
11	10	mpteq2ia	⊢ ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) )
12	11	a1i	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) )
13	12	rneqd	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) )
14	13	infeq1d	⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) , ℝ* , < ) )
15	6 14	eqtrd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) , ℝ* , < ) )