Metamath Proof Explorer

Theorem climeldmeqmpt3

Description: Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 climeldmeqmpt3.k 
 |-  F/ k ph
2 climeldmeqmpt3.m 
 |-  ( ph -> M e. ZZ )
3 climeldmeqmpt3.z 
 |-  Z = ( ZZ>= ` M )
4 climeldmeqmpt3.a 
 |-  ( ph -> A e. V )
5 climeldmeqmpt3.c 
 |-  ( ph -> C e. W )
6 climeldmeqmpt3.i 
 |-  ( ph -> Z C_ A )
7 climeldmeqmpt3.s 
 |-  ( ph -> Z C_ C )
8 climeldmeqmpt3.b 
 |-  ( ( ph /\ k e. Z ) -> B e. U )
9 climeldmeqmpt3.e 
 |-  ( ( ph /\ k e. Z ) -> B = D )
10 4 mptexd 
 |-  ( ph -> ( k e. A |-> B ) e. _V )
11 5 mptexd 
 |-  ( ph -> ( k e. C |-> D ) e. _V )
12 nfv 
 |-  F/ k j e. Z
13 1 12 nfan 
 |-  F/ k ( ph /\ j e. Z )
14 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
15 nfcv 
 |-  F/_ k j
16 15 nfcsb1 
 |-  F/_ k [_ j / k ]_ D
17 14 16 nfeq 
 |-  F/ k [_ j / k ]_ B = [_ j / k ]_ D
18 13 17 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ B = [_ j / k ]_ D )
19 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
20 19 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
21 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
22 csbeq1a 
 |-  ( k = j -> D = [_ j / k ]_ D )
23 21 22 eqeq12d 
 |-  ( k = j -> ( B = D <-> [_ j / k ]_ B = [_ j / k ]_ D ) )
24 20 23 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> B = D ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ B = [_ j / k ]_ D ) ) )
25 18 24 9 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ B = [_ j / k ]_ D )
26 6 sselda 
 |-  ( ( ph /\ j e. Z ) -> j e. A )
27 nfcv 
 |-  F/_ k U
28 14 27 nfel 
 |-  F/ k [_ j / k ]_ B e. U
29 13 28 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. U )
30 21 eleq1d 
 |-  ( k = j -> ( B e. U <-> [_ j / k ]_ B e. U ) )
31 20 30 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> B e. U ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. U ) ) )
32 29 31 8 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. U )
33 15 nfcsb1 
 |-  F/_ k [_ j / k ]_ B
34 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
35 15 33 21 34 fvmptf 
 |-  ( ( j e. A /\ [_ j / k ]_ B e. U ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
36 26 32 35 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
37 7 sselda 
 |-  ( ( ph /\ j e. Z ) -> j e. C )
38 25 32 eqeltrrd 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ D e. U )
39 eqid 
 |-  ( k e. C |-> D ) = ( k e. C |-> D )
40 15 16 22 39 fvmptf 
 |-  ( ( j e. C /\ [_ j / k ]_ D e. U ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
41 37 38 40 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
42 25 36 41 3eqtr4d 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. A |-> B ) ` j ) = ( ( k e. C |-> D ) ` j ) )
43 3 10 11 2 42 climeldmeq 
 |-  ( ph -> ( ( k e. A |-> B ) e. dom ~~> <-> ( k e. C |-> D ) e. dom ~~> ) )