Metamath Proof Explorer

Theorem climfveqmpt3

Description: Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 climfveqmpt3.k 
 |-  F/ k ph
2 climfveqmpt3.m 
 |-  ( ph -> M e. ZZ )
3 climfveqmpt3.z 
 |-  Z = ( ZZ>= ` M )
4 climfveqmpt3.a 
 |-  ( ph -> A e. V )
5 climfveqmpt3.c 
 |-  ( ph -> C e. W )
6 climfveqmpt3.i 
 |-  ( ph -> Z C_ A )
7 climfveqmpt3.s 
 |-  ( ph -> Z C_ C )
8 climfveqmpt3.b 
 |-  ( ( ph /\ k e. Z ) -> B e. U )
9 climfveqmpt3.d 
 |-  ( ( 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 nfcv 
 |-  F/_ k j
15 14 nfcsb1 
 |-  F/_ k [_ j / k ]_ B
16 14 nfcsb1 
 |-  F/_ k [_ j / k ]_ D
17 15 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 adantr 
 |-  ( ( ph /\ j e. Z ) -> Z C_ A )
27 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
28 26 27 sseldd 
 |-  ( ( ph /\ j e. Z ) -> j e. A )
29 nfcv 
 |-  F/_ k U
30 15 29 nfel 
 |-  F/ k [_ j / k ]_ B e. U
31 13 30 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. U )
32 21 eleq1d 
 |-  ( k = j -> ( B e. U <-> [_ j / k ]_ B e. U ) )
33 20 32 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> B e. U ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. U ) ) )
34 31 33 8 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. U )
35 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
36 14 15 21 35 fvmptf 
 |-  ( ( j e. A /\ [_ j / k ]_ B e. U ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
37 28 34 36 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. A |-> B ) ` j ) = [_ j / k ]_ B )
38 7 adantr 
 |-  ( ( ph /\ j e. Z ) -> Z C_ C )
39 38 27 sseldd 
 |-  ( ( ph /\ j e. Z ) -> j e. C )
40 25 34 eqeltrrd 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ D e. U )
41 eqid 
 |-  ( k e. C |-> D ) = ( k e. C |-> D )
42 14 16 22 41 fvmptf 
 |-  ( ( j e. C /\ [_ j / k ]_ D e. U ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
43 39 40 42 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. C |-> D ) ` j ) = [_ j / k ]_ D )
44 25 37 43 3eqtr4d 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. A |-> B ) ` j ) = ( ( k e. C |-> D ) ` j ) )
45 3 10 11 2 44 climfveq 
 |-  ( ph -> ( ~~> ` ( k e. A |-> B ) ) = ( ~~> ` ( k e. C |-> D ) ) )