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

Metamath Proof Explorer

Theorem climfveqf

Proof