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	|- F/ j ph
	limsupequzmpt.m	|- ( ph -> M e. ZZ )
	limsupequzmpt.n	|- ( ph -> N e. ZZ )
	limsupequzmpt.a	|- A = ( ZZ>= ` M )
	limsupequzmpt.b	|- B = ( ZZ>= ` N )
	limsupequzmpt.c	|- ( ( ph /\ j e. A ) -> C e. V )
	limsupequzmpt.d	|- ( ( ph /\ j e. B ) -> C e. W )
Assertion	limsupequzmpt	|- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupequzmpt.j	|- F/ j ph
2		limsupequzmpt.m	|- ( ph -> M e. ZZ )
3		limsupequzmpt.n	|- ( ph -> N e. ZZ )
4		limsupequzmpt.a	|- A = ( ZZ>= ` M )
5		limsupequzmpt.b	|- B = ( ZZ>= ` N )
6		limsupequzmpt.c	|- ( ( ph /\ j e. A ) -> C e. V )
7		limsupequzmpt.d	|- ( ( ph /\ j e. B ) -> C e. W )
8		eqid	|- if ( M <_ N , N , M ) = if ( M <_ N , N , M )
9	1 2 3 4 5 6 7 8	limsupequzmptlem	|- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )