Metamath Proof Explorer

Theorem climfveqmpt2

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

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

Proof

Step Hyp Ref Expression
1 climfveqmpt2.k 
 |-  F/ k ph
2 climfveqmpt2.m 
 |-  ( ph -> M e. ZZ )
3 climfveqmpt2.z 
 |-  Z = ( ZZ>= ` M )
4 climfveqmpt2.a 
 |-  ( ph -> A e. V )
5 climfveqmpt2.c 
 |-  ( ph -> B e. W )
6 climfveqmpt2.s 
 |-  ( ph -> Z C_ A )
7 climfveqmpt2.i 
 |-  ( ph -> Z C_ B )
8 climfveqmpt2.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 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
15 14 fvmpt2 
 |-  ( ( k e. A /\ C e. U ) -> ( ( k e. A |-> C ) ` k ) = C )
16 13 8 15 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. A |-> C ) ` k ) = C )
17 7 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. B )
18 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
19 18 fvmpt2 
 |-  ( ( k e. B /\ C e. U ) -> ( ( k e. B |-> C ) ` k ) = C )
20 17 8 19 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. B |-> C ) ` k ) = C )
21 16 20 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. A |-> C ) ` k ) = ( ( k e. B |-> C ) ` k ) )
22 1 9 10 3 11 12 2 21 climfveqf 
 |-  ( ph -> ( ~~> ` ( k e. A |-> C ) ) = ( ~~> ` ( k e. B |-> C ) ) )