Metamath Proof Explorer

Theorem climfveqmpt

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climfveqmpt.k 
|- F/ k ph
climfveqmpt.m 
|- ( ph -> M e. ZZ )
climfveqmpt.z 
|- Z = ( ZZ>= ` M )
climfveqmpt.A 
|- ( ph -> A e. R )
climfveqmpt.i 
|- ( ph -> Z C_ A )
climfveqmpt.b 
|- ( ( ph /\ k e. A ) -> B e. V )
climfveqmpt.t 
|- ( ph -> C e. S )
climfveqmpt.l 
|- ( ph -> Z C_ C )
climfveqmpt.c 
|- ( ( ph /\ k e. C ) -> D e. W )
climfveqmpt.e 
|- ( ( ph /\ k e. Z ) -> B = D )
Assertion climfveqmpt 
|- ( ph -> ( ~~> ` ( k e. A |-> B ) ) = ( ~~> ` ( k e. C |-> D ) ) )

Proof

Step Hyp Ref Expression
1 climfveqmpt.k 
 |-  F/ k ph
2 climfveqmpt.m 
 |-  ( ph -> M e. ZZ )
3 climfveqmpt.z 
 |-  Z = ( ZZ>= ` M )
4 climfveqmpt.A 
 |-  ( ph -> A e. R )
5 climfveqmpt.i 
 |-  ( ph -> Z C_ A )
6 climfveqmpt.b 
 |-  ( ( ph /\ k e. A ) -> B e. V )
7 climfveqmpt.t 
 |-  ( ph -> C e. S )
8 climfveqmpt.l 
 |-  ( ph -> Z C_ C )
9 climfveqmpt.c 
 |-  ( ( ph /\ k e. C ) -> D e. W )
10 climfveqmpt.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 nfcv 
 |-  F/_ k j
16 15 nfcsb1 
 |-  F/_ k [_ j / k ]_ B
17 15 nfcsb1 
 |-  F/_ k [_ j / k ]_ D
18 16 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 adantr 
 |-  ( ( ph /\ j e. Z ) -> Z C_ A )
28 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
29 27 28 sseldd 
 |-  ( ( ph /\ j e. Z ) -> j e. A )
30 simpr 
 |-  ( ( ph /\ j e. A ) -> j e. A )
31 nfv 
 |-  F/ k j e. A
32 1 31 nfan 
 |-  F/ k ( ph /\ j e. A )
33 nfcv 
 |-  F/_ k V
34 16 33 nfel 
 |-  F/ k [_ j / k ]_ B e. V
35 32 34 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. V )
36 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
37 36 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
38 22 eleq1d 
 |-  ( k = j -> ( B e. V <-> [_ j / k ]_ B e. V ) )
39 37 38 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> B e. V ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. V ) ) )
40 35 39 6 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. V )
41 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
42 15 16 22 41 fvmptf 
 |-  ( ( j e. A /\ [_ j / k ]_ B e. V ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
43 30 40 42 syl2anc 
 |-  ( ( ph /\ j e. A ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
44 29 43 syldan 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
45 8 adantr 
 |-  ( ( ph /\ j e. Z ) -> Z C_ C )
46 45 28 sseldd 
 |-  ( ( ph /\ j e. Z ) -> j e. C )
47 simpr 
 |-  ( ( ph /\ j e. C ) -> j e. C )
48 nfv 
 |-  F/ k j e. C
49 1 48 nfan 
 |-  F/ k ( ph /\ j e. C )
50 nfcv 
 |-  F/_ k W
51 17 50 nfel 
 |-  F/ k [_ j / k ]_ D e. W
52 49 51 nfim 
 |-  F/ k ( ( ph /\ j e. C ) -> [_ j / k ]_ D e. W )
53 eleq1w 
 |-  ( k = j -> ( k e. C <-> j e. C ) )
54 53 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. C ) <-> ( ph /\ j e. C ) ) )
55 23 eleq1d 
 |-  ( k = j -> ( D e. W <-> [_ j / k ]_ D e. W ) )
56 54 55 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. C ) -> D e. W ) <-> ( ( ph /\ j e. C ) -> [_ j / k ]_ D e. W ) ) )
57 52 56 9 chvarfv 
 |-  ( ( ph /\ j e. C ) -> [_ j / k ]_ D e. W )
58 eqid 
 |-  ( k e. C |-> D ) = ( k e. C |-> D )
59 15 17 23 58 fvmptf 
 |-  ( ( j e. C /\ [_ j / k ]_ D e. W ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
60 47 57 59 syl2anc 
 |-  ( ( ph /\ j e. C ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
61 46 60 syldan 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
62 26 44 61 3eqtr4d 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. A |-> B ) ` j ) = ( ( k e. C |-> D ) ` j ) )
63 3 11 12 2 62 climfveq 
 |-  ( ph -> ( ~~> ` ( k e. A |-> B ) ) = ( ~~> ` ( k e. C |-> D ) ) )