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

Metamath Proof Explorer

Theorem climeldmeqmpt2

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

Ref Expression
Hypotheses climeldmeqmpt2.k 
|- F/ k ph
climeldmeqmpt2.m 
|- ( ph -> M e. ZZ )
climeldmeqmpt2.z 
|- Z = ( ZZ>= ` M )
climeldmeqmpt2.a 
|- ( ph -> A e. W )
climeldmeqmpt2.t 
|- ( ph -> B e. V )
climeldmeqmpt2.i 
|- ( ph -> Z C_ A )
climeldmeqmpt2.l 
|- ( ph -> Z C_ B )
climeldmeqmpt2.b 
|- ( ( ph /\ k e. Z ) -> C e. U )
Assertion climeldmeqmpt2 
|- ( ph -> ( ( k e. A |-> C ) e. dom ~~> <-> ( k e. B |-> C ) e. dom ~~> ) )

Proof

Step Hyp Ref Expression
1 climeldmeqmpt2.k 
 |-  F/ k ph
2 climeldmeqmpt2.m 
 |-  ( ph -> M e. ZZ )
3 climeldmeqmpt2.z 
 |-  Z = ( ZZ>= ` M )
4 climeldmeqmpt2.a 
 |-  ( ph -> A e. W )
5 climeldmeqmpt2.t 
 |-  ( ph -> B e. V )
6 climeldmeqmpt2.i 
 |-  ( ph -> Z C_ A )
7 climeldmeqmpt2.l 
 |-  ( ph -> Z C_ B )
8 climeldmeqmpt2.b 
 |-  ( ( ph /\ k e. Z ) -> C e. U )
9 nfmpt1 
 |-  F/_ k ( k e. A |-> C )
10 nfmpt1 
 |-  F/_ k ( k e. B |-> C )
11 4 mptexd 
 |-  ( ph -> ( k e. A |-> C ) e. _V )
12 5 mptexd 
 |-  ( ph -> ( k e. B |-> C ) e. _V )
13 6 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. A )
14 fvmpt4 
 |-  ( ( k e. A /\ C e. U ) -> ( ( k e. A |-> C ) ` k ) = C )
15 13 8 14 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. A |-> C ) ` k ) = C )
16 7 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. B )
17 fvmpt4 
 |-  ( ( k e. B /\ C e. U ) -> ( ( k e. B |-> C ) ` k ) = C )
18 16 8 17 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. B |-> C ) ` k ) = C )
19 15 18 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. A |-> C ) ` k ) = ( ( k e. B |-> C ) ` k ) )
20 1 9 10 3 11 12 2 19 climeldmeqf 
 |-  ( ph -> ( ( k e. A |-> C ) e. dom ~~> <-> ( k e. B |-> C ) e. dom ~~> ) )