Theorem limsupequzmpt

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupequzmpt.j	⊢ Ⅎ 𝑗 𝜑
	limsupequzmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupequzmpt.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	limsupequzmpt.a	⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
	limsupequzmpt.b	⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
	limsupequzmpt.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	limsupequzmpt.d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
Assertion	limsupequzmpt	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupequzmpt.j	⊢ Ⅎ 𝑗 𝜑
2		limsupequzmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupequzmpt.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		limsupequzmpt.a	⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
5		limsupequzmpt.b	⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
6		limsupequzmpt.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
7		limsupequzmpt.d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
8		eqid	⊢ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 )
9	1 2 3 4 5 6 7 8	limsupequzmptlem	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )