Metamath Proof Explorer

Theorem climeldmeq

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climeldmeq.z 
|- Z = ( ZZ>= ` M )
climeldmeq.f 
|- ( ph -> F e. V )
climeldmeq.g 
|- ( ph -> G e. W )
climeldmeq.m 
|- ( ph -> M e. ZZ )
climeldmeq.e 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
Assertion climeldmeq 
|- ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )

Proof

Step Hyp Ref Expression
1 climeldmeq.z 
 |-  Z = ( ZZ>= ` M )
2 climeldmeq.f 
 |-  ( ph -> F e. V )
3 climeldmeq.g 
 |-  ( ph -> G e. W )
4 climeldmeq.m 
 |-  ( ph -> M e. ZZ )
5 climeldmeq.e 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
6 3 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> G e. W )
7 fvexd 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( ~~> ` F ) e. _V )
8 climdm 
 |-  ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
9 8 a1i 
 |-  ( ph -> ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) ) )
10 9 biimpa 
 |-  ( ( ph /\ F e. dom ~~> ) -> F ~~> ( ~~> ` F ) )
11 1 2 3 4 5 climeq 
 |-  ( ph -> ( F ~~> ( ~~> ` F ) <-> G ~~> ( ~~> ` F ) ) )
12 11 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( F ~~> ( ~~> ` F ) <-> G ~~> ( ~~> ` F ) ) )
13 10 12 mpbid 
 |-  ( ( ph /\ F e. dom ~~> ) -> G ~~> ( ~~> ` F ) )
14 breldmg 
 |-  ( ( G e. W /\ ( ~~> ` F ) e. _V /\ G ~~> ( ~~> ` F ) ) -> G e. dom ~~> )
15 6 7 13 14 syl3anc 
 |-  ( ( ph /\ F e. dom ~~> ) -> G e. dom ~~> )
16 15 ex 
 |-  ( ph -> ( F e. dom ~~> -> G e. dom ~~> ) )
17 2 adantr 
 |-  ( ( ph /\ G e. dom ~~> ) -> F e. V )
18 fvexd 
 |-  ( ( ph /\ G e. dom ~~> ) -> ( ~~> ` G ) e. _V )
19 climdm 
 |-  ( G e. dom ~~> <-> G ~~> ( ~~> ` G ) )
20 19 biimpi 
 |-  ( G e. dom ~~> -> G ~~> ( ~~> ` G ) )
21 20 adantl 
 |-  ( ( ph /\ G e. dom ~~> ) -> G ~~> ( ~~> ` G ) )
22 5 eqcomd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( F ` k ) )
23 1 3 2 4 22 climeq 
 |-  ( ph -> ( G ~~> ( ~~> ` G ) <-> F ~~> ( ~~> ` G ) ) )
24 23 adantr 
 |-  ( ( ph /\ G e. dom ~~> ) -> ( G ~~> ( ~~> ` G ) <-> F ~~> ( ~~> ` G ) ) )
25 21 24 mpbid 
 |-  ( ( ph /\ G e. dom ~~> ) -> F ~~> ( ~~> ` G ) )
26 breldmg 
 |-  ( ( F e. V /\ ( ~~> ` G ) e. _V /\ F ~~> ( ~~> ` G ) ) -> F e. dom ~~> )
27 17 18 25 26 syl3anc 
 |-  ( ( ph /\ G e. dom ~~> ) -> F e. dom ~~> )
28 27 ex 
 |-  ( ph -> ( G e. dom ~~> -> F e. dom ~~> ) )
29 16 28 impbid 
 |-  ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )