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

Metamath Proof Explorer

Theorem lmclim2

Description: A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses lmclim2.2 
|- ( ph -> D e. ( Met ` X ) )
lmclim2.3 
|- ( ph -> F : NN --> X )
lmclim2.4 
|- J = ( MetOpen ` D )
lmclim2.5 
|- G = ( x e. NN |-> ( ( F ` x ) D Y ) )
lmclim2.6 
|- ( ph -> Y e. X )
Assertion lmclim2 
|- ( ph -> ( F ( ~~>t ` J ) Y <-> G ~~> 0 ) )

Proof

Step Hyp Ref Expression
1 lmclim2.2 
 |-  ( ph -> D e. ( Met ` X ) )
2 lmclim2.3 
 |-  ( ph -> F : NN --> X )
3 lmclim2.4 
 |-  J = ( MetOpen ` D )
4 lmclim2.5 
 |-  G = ( x e. NN |-> ( ( F ` x ) D Y ) )
5 lmclim2.6 
 |-  ( ph -> Y e. X )
6 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
7 1 6 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
8 nnuz 
 |-  NN = ( ZZ>= ` 1 )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
11 3 7 8 9 10 2 lmmbrf 
 |-  ( ph -> ( F ( ~~>t ` J ) Y <-> ( Y e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x ) ) )
12 nnex 
 |-  NN e. _V
13 12 mptex 
 |-  ( x e. NN |-> ( ( F ` x ) D Y ) ) e. _V
14 4 13 eqeltri 
 |-  G e. _V
15 14 a1i 
 |-  ( ph -> G e. _V )
16 fveq2 
 |-  ( x = k -> ( F ` x ) = ( F ` k ) )
17 16 oveq1d 
 |-  ( x = k -> ( ( F ` x ) D Y ) = ( ( F ` k ) D Y ) )
18 ovex 
 |-  ( ( F ` k ) D Y ) e. _V
19 17 4 18 fvmpt 
 |-  ( k e. NN -> ( G ` k ) = ( ( F ` k ) D Y ) )
20 19 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) = ( ( F ` k ) D Y ) )
21 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> D e. ( Met ` X ) )
22 2 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )
23 5 adantr 
 |-  ( ( ph /\ k e. NN ) -> Y e. X )
24 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ Y e. X ) -> ( ( F ` k ) D Y ) e. RR )
25 21 22 23 24 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D Y ) e. RR )
26 25 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D Y ) e. CC )
27 8 9 15 20 26 clim0c 
 |-  ( ph -> ( G ~~> 0 <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) D Y ) ) < x ) )
28 eluznn 
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
29 metge0 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ Y e. X ) -> 0 <_ ( ( F ` k ) D Y ) )
30 21 22 23 29 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( ( F ` k ) D Y ) )
31 25 30 absidd 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( ( F ` k ) D Y ) ) = ( ( F ` k ) D Y ) )
32 31 breq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( abs ` ( ( F ` k ) D Y ) ) < x <-> ( ( F ` k ) D Y ) < x ) )
33 28 32 sylan2 
 |-  ( ( ph /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( F ` k ) D Y ) ) < x <-> ( ( F ` k ) D Y ) < x ) )
34 33 anassrs 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( F ` k ) D Y ) ) < x <-> ( ( F ` k ) D Y ) < x ) )
35 34 ralbidva 
 |-  ( ( ph /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) D Y ) ) < x <-> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x ) )
36 35 rexbidva 
 |-  ( ph -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) D Y ) ) < x <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x ) )
37 36 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) D Y ) ) < x <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x ) )
38 5 biantrurd 
 |-  ( ph -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x <-> ( Y e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x ) ) )
39 27 37 38 3bitrrd 
 |-  ( ph -> ( ( Y e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D Y ) < x ) <-> G ~~> 0 ) )
40 11 39 bitrd 
 |-  ( ph -> ( F ( ~~>t ` J ) Y <-> G ~~> 0 ) )