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