climfveqf

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

	Ref	Expression
Hypotheses	climfveqf.p	\|- F/ k ph
	climfveqf.n	\|- F/_ k F
	climfveqf.o	\|- F/_ k G
	climfveqf.z	\|- Z = ( ZZ>= ` M )
	climfveqf.f	\|- ( ph -> F e. V )
	climfveqf.g	\|- ( ph -> G e. W )
	climfveqf.m	\|- ( ph -> M e. ZZ )
	climfveqf.e	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
Assertion	climfveqf	\|- ( ph -> ( ~~> ` F ) = ( ~~> ` G ) )

Proof

Step	Hyp	Ref	Expression
1		climfveqf.p	\|- F/ k ph
2		climfveqf.n	\|- F/_ k F
3		climfveqf.o	\|- F/_ k G
4		climfveqf.z	\|- Z = ( ZZ>= ` M )
5		climfveqf.f	\|- ( ph -> F e. V )
6		climfveqf.g	\|- ( ph -> G e. W )
7		climfveqf.m	\|- ( ph -> M e. ZZ )
8		climfveqf.e	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
9		climdm	\|- ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
10	9	biimpi	\|- ( F e. dom ~~> -> F ~~> ( ~~> ` F ) )
11	10	adantl	\|- ( ( ph /\ F e. dom ~~> ) -> F ~~> ( ~~> ` F ) )
12	11 9	sylibr	\|- ( ( ph /\ F e. dom ~~> ) -> F e. dom ~~> )
13		nfcv	\|- F/_ k j
14	13	nfel1	\|- F/ k j e. Z
15	1 14	nfan	\|- F/ k ( ph /\ j e. Z )
16	2 13	nffv	\|- F/_ k ( F ` j )
17	3 13	nffv	\|- F/_ k ( G ` j )
18	16 17	nfeq	\|- F/ k ( F ` j ) = ( G ` j )
19	15 18	nfim	\|- F/ k ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` j ) )
20		eleq1w	\|- ( k = j -> ( k e. Z <-> j e. Z ) )
21	20	anbi2d	\|- ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
22		fveq2	\|- ( k = j -> ( F ` k ) = ( F ` j ) )
23		fveq2	\|- ( k = j -> ( G ` k ) = ( G ` j ) )
24	22 23	eqeq12d	\|- ( k = j -> ( ( F ` k ) = ( G ` k ) <-> ( F ` j ) = ( G ` j ) ) )
25	21 24	imbi12d	\|- ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` j ) ) ) )
26	19 25 8	chvarfv	\|- ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` j ) )
27	4 5 6 7 26	climeldmeq	\|- ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )
28	27	adantr	\|- ( ( ph /\ F e. dom ~~> ) -> ( F e. dom ~~> <-> G e. dom ~~> ) )
29	12 28	mpbid	\|- ( ( ph /\ F e. dom ~~> ) -> G e. dom ~~> )
30		climdm	\|- ( G e. dom ~~> <-> G ~~> ( ~~> ` G ) )
31	29 30	sylib	\|- ( ( ph /\ F e. dom ~~> ) -> G ~~> ( ~~> ` G ) )
32	6	adantr	\|- ( ( ph /\ F e. dom ~~> ) -> G e. W )
33	5	adantr	\|- ( ( ph /\ F e. dom ~~> ) -> F e. V )
34	7	adantr	\|- ( ( ph /\ F e. dom ~~> ) -> M e. ZZ )
35	26	eqcomd	\|- ( ( ph /\ j e. Z ) -> ( G ` j ) = ( F ` j ) )
36	35	adantlr	\|- ( ( ( ph /\ F e. dom ~~> ) /\ j e. Z ) -> ( G ` j ) = ( F ` j ) )
37	4 32 33 34 36	climeq	\|- ( ( ph /\ F e. dom ~~> ) -> ( G ~~> ( ~~> ` G ) <-> F ~~> ( ~~> ` G ) ) )
38	31 37	mpbid	\|- ( ( ph /\ F e. dom ~~> ) -> F ~~> ( ~~> ` G ) )
39		climuni	\|- ( ( F ~~> ( ~~> ` F ) /\ F ~~> ( ~~> ` G ) ) -> ( ~~> ` F ) = ( ~~> ` G ) )
40	11 38 39	syl2anc	\|- ( ( ph /\ F e. dom ~~> ) -> ( ~~> ` F ) = ( ~~> ` G ) )
41		ndmfv	\|- ( -. F e. dom ~~> -> ( ~~> ` F ) = (/) )
42	41	adantl	\|- ( ( ph /\ -. F e. dom ~~> ) -> ( ~~> ` F ) = (/) )
43		simpr	\|- ( ( ph /\ -. F e. dom ~~> ) -> -. F e. dom ~~> )
44	27	adantr	\|- ( ( ph /\ -. F e. dom ~~> ) -> ( F e. dom ~~> <-> G e. dom ~~> ) )
45	43 44	mtbid	\|- ( ( ph /\ -. F e. dom ~~> ) -> -. G e. dom ~~> )
46		ndmfv	\|- ( -. G e. dom ~~> -> ( ~~> ` G ) = (/) )
47	45 46	syl	\|- ( ( ph /\ -. F e. dom ~~> ) -> ( ~~> ` G ) = (/) )
48	42 47	eqtr4d	\|- ( ( ph /\ -. F e. dom ~~> ) -> ( ~~> ` F ) = ( ~~> ` G ) )
49	40 48	pm2.61dan	\|- ( ph -> ( ~~> ` F ) = ( ~~> ` G ) )

Metamath Proof Explorer

Theorem climfveqf

Proof