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	$$⊢Ⅎj\phi$$
	limsupequzmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupequzmpt.n	$$⊢\phi \to N\in \mathbb{Z}$$
	limsupequzmpt.a	$$⊢A={\mathbb{Z}}_{\ge M}$$
	limsupequzmpt.b	$$⊢B={\mathbb{Z}}_{\ge N}$$
	limsupequzmpt.c	$$⊢\left(\phi \wedge j\in A\right)\to C\in V$$
	limsupequzmpt.d	$$⊢\left(\phi \wedge j\in B\right)\to C\in W$$
Assertion	limsupequzmpt	$$⊢\phi \to \mathrm{lim\; sup}\left(\left(j\in A⟼C\right)\right)=\mathrm{lim\; sup}\left(\left(j\in B⟼C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupequzmpt.j	$$⊢Ⅎj\phi$$
2		limsupequzmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		limsupequzmpt.n	$$⊢\phi \to N\in \mathbb{Z}$$
4		limsupequzmpt.a	$$⊢A={\mathbb{Z}}_{\ge M}$$
5		limsupequzmpt.b	$$⊢B={\mathbb{Z}}_{\ge N}$$
6		limsupequzmpt.c	$$⊢\left(\phi \wedge j\in A\right)\to C\in V$$
7		limsupequzmpt.d	$$⊢\left(\phi \wedge j\in B\right)\to C\in W$$
8		eqid	$$⊢if\left(M\le N,N,M\right)=if\left(M\le N,N,M\right)$$
9	1 2 3 4 5 6 7 8	limsupequzmptlem	$$⊢\phi \to \mathrm{lim\; sup}\left(\left(j\in A⟼C\right)\right)=\mathrm{lim\; sup}\left(\left(j\in B⟼C\right)\right)$$