Theorem climeqmpt

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

	Ref	Expression
Hypotheses	climeqmpt.x	|- F/ x ph
	climeqmpt.a	|- ( ph -> A e. V )
	climeqmpt.b	|- ( ph -> B e. W )
	climeqmpt.m	|- ( ph -> M e. ZZ )
	climeqmpt.z	|- Z = ( ZZ>= ` M )
	climeqmpt.s	|- ( ph -> Z C_ A )
	climeqmpt.t	|- ( ph -> Z C_ B )
	climeqmpt.c	|- ( ( ph /\ x e. Z ) -> C e. U )
Assertion	climeqmpt	|- ( ph -> ( ( x e. A |-> C ) ~~> D <-> ( x e. B |-> C ) ~~> D ) )

Proof

Step	Hyp	Ref	Expression
1		climeqmpt.x	|- F/ x ph
2		climeqmpt.a	|- ( ph -> A e. V )
3		climeqmpt.b	|- ( ph -> B e. W )
4		climeqmpt.m	|- ( ph -> M e. ZZ )
5		climeqmpt.z	|- Z = ( ZZ>= ` M )
6		climeqmpt.s	|- ( ph -> Z C_ A )
7		climeqmpt.t	|- ( ph -> Z C_ B )
8		climeqmpt.c	|- ( ( ph /\ x e. Z ) -> C e. U )
9		nfmpt1	|- F/_ x ( x e. A |-> C )
10		nfmpt1	|- F/_ x ( x e. B |-> C )
11	2	mptexd	|- ( ph -> ( x e. A |-> C ) e. _V )
12	3	mptexd	|- ( ph -> ( x e. B |-> C ) e. _V )
13	6	adantr	|- ( ( ph /\ x e. Z ) -> Z C_ A )
14		simpr	|- ( ( ph /\ x e. Z ) -> x e. Z )
15	13 14	sseldd	|- ( ( ph /\ x e. Z ) -> x e. A )
16		eqid	|- ( x e. A |-> C ) = ( x e. A |-> C )
17	16	fvmpt2	|- ( ( x e. A /\ C e. U ) -> ( ( x e. A |-> C ) ` x ) = C )
18	15 8 17	syl2anc	|- ( ( ph /\ x e. Z ) -> ( ( x e. A |-> C ) ` x ) = C )
19	7	adantr	|- ( ( ph /\ x e. Z ) -> Z C_ B )
20	19 14	sseldd	|- ( ( ph /\ x e. Z ) -> x e. B )
21		eqid	|- ( x e. B |-> C ) = ( x e. B |-> C )
22	21	fvmpt2	|- ( ( x e. B /\ C e. U ) -> ( ( x e. B |-> C ) ` x ) = C )
23	20 8 22	syl2anc	|- ( ( ph /\ x e. Z ) -> ( ( x e. B |-> C ) ` x ) = C )
24	23	eqcomd	|- ( ( ph /\ x e. Z ) -> C = ( ( x e. B |-> C ) ` x ) )
25	18 24	eqtrd	|- ( ( ph /\ x e. Z ) -> ( ( x e. A |-> C ) ` x ) = ( ( x e. B |-> C ) ` x ) )
26	1 9 10 4 5 11 12 25	climeqf	|- ( ph -> ( ( x e. A |-> C ) ~~> D <-> ( x e. B |-> C ) ~~> D ) )