Metamath Proof Explorer

Theorem climfveq

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

Ref Expression
Hypotheses climfveq.1 
|- Z = ( ZZ>= ` M )
climfveq.2 
|- ( ph -> F e. V )
climfveq.3 
|- ( ph -> G e. W )
climfveq.4 
|- ( ph -> M e. ZZ )
climfveq.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
Assertion climfveq 
|- ( ph -> ( ~~> ` F ) = ( ~~> ` G ) )

Proof

Step Hyp Ref Expression
1 climfveq.1 
 |-  Z = ( ZZ>= ` M )
2 climfveq.2 
 |-  ( ph -> F e. V )
3 climfveq.3 
 |-  ( ph -> G e. W )
4 climfveq.4 
 |-  ( ph -> M e. ZZ )
5 climfveq.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
6 climdm 
 |-  ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
7 6 biimpi 
 |-  ( F e. dom ~~> -> F ~~> ( ~~> ` F ) )
8 7 adantl 
 |-  ( ( ph /\ F e. dom ~~> ) -> F ~~> ( ~~> ` F ) )
9 8 6 sylibr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F e. dom ~~> )
10 1 2 3 4 5 climeldmeq 
 |-  ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )
11 10 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( F e. dom ~~> <-> G e. dom ~~> ) )
12 9 11 mpbid 
 |-  ( ( ph /\ F e. dom ~~> ) -> G e. dom ~~> )
13 climdm 
 |-  ( G e. dom ~~> <-> G ~~> ( ~~> ` G ) )
14 12 13 sylib 
 |-  ( ( ph /\ F e. dom ~~> ) -> G ~~> ( ~~> ` G ) )
15 3 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> G e. W )
16 2 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F e. V )
17 4 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> M e. ZZ )
18 5 eqcomd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( F ` k ) )
19 18 adantlr 
 |-  ( ( ( ph /\ F e. dom ~~> ) /\ k e. Z ) -> ( G ` k ) = ( F ` k ) )
20 1 15 16 17 19 climeq 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( G ~~> ( ~~> ` G ) <-> F ~~> ( ~~> ` G ) ) )
21 14 20 mpbid 
 |-  ( ( ph /\ F e. dom ~~> ) -> F ~~> ( ~~> ` G ) )
22 climuni 
 |-  ( ( F ~~> ( ~~> ` F ) /\ F ~~> ( ~~> ` G ) ) -> ( ~~> ` F ) = ( ~~> ` G ) )
23 8 21 22 syl2anc 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( ~~> ` F ) = ( ~~> ` G ) )
24 ndmfv 
 |-  ( -. F e. dom ~~> -> ( ~~> ` F ) = (/) )
25 24 adantl 
 |-  ( ( ph /\ -. F e. dom ~~> ) -> ( ~~> ` F ) = (/) )
26 simpr 
 |-  ( ( ph /\ -. F e. dom ~~> ) -> -. F e. dom ~~> )
27 10 adantr 
 |-  ( ( ph /\ -. F e. dom ~~> ) -> ( F e. dom ~~> <-> G e. dom ~~> ) )
28 26 27 mtbid 
 |-  ( ( ph /\ -. F e. dom ~~> ) -> -. G e. dom ~~> )
29 ndmfv 
 |-  ( -. G e. dom ~~> -> ( ~~> ` G ) = (/) )
30 28 29 syl 
 |-  ( ( ph /\ -. F e. dom ~~> ) -> ( ~~> ` G ) = (/) )
31 25 30 eqtr4d 
 |-  ( ( ph /\ -. F e. dom ~~> ) -> ( ~~> ` F ) = ( ~~> ` G ) )
32 23 31 pm2.61dan 
 |-  ( ph -> ( ~~> ` F ) = ( ~~> ` G ) )