This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climeqmpt

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

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

Proof

Step Hyp Ref Expression
1 climeqmpt.x 
 |-  F/ x ph
2 climeqmpt.a 
 |-  ( ph -> A e. V )
3 climeqmpt.b 
 |-  ( ph -> B e. W )
4 climeqmpt.m 
 |-  ( ph -> M e. ZZ )
5 climeqmpt.z 
 |-  Z = ( ZZ>= ` M )
6 climeqmpt.s 
 |-  ( ph -> Z C_ A )
7 climeqmpt.t 
 |-  ( ph -> Z C_ B )
8 climeqmpt.c 
 |-  ( ( ph /\ x e. Z ) -> C e. U )
9 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
10 nfmpt1 
 |-  F/_ x ( x e. B |-> C )
11 2 mptexd 
 |-  ( ph -> ( x e. A |-> C ) e. _V )
12 3 mptexd 
 |-  ( ph -> ( x e. B |-> C ) e. _V )
13 6 adantr 
 |-  ( ( ph /\ x e. Z ) -> Z C_ A )
14 simpr 
 |-  ( ( ph /\ x e. Z ) -> x e. Z )
15 13 14 sseldd 
 |-  ( ( ph /\ x e. Z ) -> x e. A )
16 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
17 16 fvmpt2 
 |-  ( ( x e. A /\ C e. U ) -> ( ( x e. A |-> C ) ` x ) = C )
18 15 8 17 syl2anc 
 |-  ( ( ph /\ x e. Z ) -> ( ( x e. A |-> C ) ` x ) = C )
19 7 adantr 
 |-  ( ( ph /\ x e. Z ) -> Z C_ B )
20 19 14 sseldd 
 |-  ( ( ph /\ x e. Z ) -> x e. B )
21 eqid 
 |-  ( x e. B |-> C ) = ( x e. B |-> C )
22 21 fvmpt2 
 |-  ( ( x e. B /\ C e. U ) -> ( ( x e. B |-> C ) ` x ) = C )
23 20 8 22 syl2anc 
 |-  ( ( ph /\ x e. Z ) -> ( ( x e. B |-> C ) ` x ) = C )
24 23 eqcomd 
 |-  ( ( ph /\ x e. Z ) -> C = ( ( x e. B |-> C ) ` x ) )
25 18 24 eqtrd 
 |-  ( ( ph /\ x e. Z ) -> ( ( x e. A |-> C ) ` x ) = ( ( x e. B |-> C ) ` x ) )
26 1 9 10 4 5 11 12 25 climeqf 
 |-  ( ph -> ( ( x e. A |-> C ) ~~> D <-> ( x e. B |-> C ) ~~> D ) )