Metamath Proof Explorer

Theorem climeldmeqmpt

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 climeldmeqmpt.k 
|- F/ k ph
climeldmeqmpt.m 
|- ( ph -> M e. ZZ )
climeldmeqmpt.z 
|- Z = ( ZZ>= ` M )
climeldmeqmpt.a 
|- ( ph -> A e. R )
climeldmeqmpt.i 
|- ( ph -> Z C_ A )
climeldmeqmpt.b 
|- ( ( ph /\ k e. A ) -> B e. V )
climeldmeqmpt.t 
|- ( ph -> C e. S )
climeldmeqmpt.l 
|- ( ph -> Z C_ C )
climeldmeqmpt.c 
|- ( ( ph /\ k e. C ) -> D e. W )
climeldmeqmpt.e 
|- ( ( ph /\ k e. Z ) -> B = D )
Assertion climeldmeqmpt 
|- ( ph -> ( ( k e. A |-> B ) e. dom ~~> <-> ( k e. C |-> D ) e. dom ~~> ) )

Proof

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