This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) )