Metamath Proof Explorer

Theorem lmle

Description: If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. (Contributed by NM, 23-Dec-2007) (Proof shortened by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmle.1 
|- Z = ( ZZ>= ` M )
lmle.3 
|- J = ( MetOpen ` D )
lmle.4 
|- ( ph -> D e. ( *Met ` X ) )
lmle.6 
|- ( ph -> M e. ZZ )
lmle.7 
|- ( ph -> F ( ~~>t ` J ) P )
lmle.8 
|- ( ph -> Q e. X )
lmle.9 
|- ( ph -> R e. RR* )
lmle.10 
|- ( ( ph /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )
Assertion lmle 
|- ( ph -> ( Q D P ) <_ R )

Proof

Step Hyp Ref Expression
1 lmle.1 
 |-  Z = ( ZZ>= ` M )
2 lmle.3 
 |-  J = ( MetOpen ` D )
3 lmle.4 
 |-  ( ph -> D e. ( *Met ` X ) )
4 lmle.6 
 |-  ( ph -> M e. ZZ )
5 lmle.7 
 |-  ( ph -> F ( ~~>t ` J ) P )
6 lmle.8 
 |-  ( ph -> Q e. X )
7 lmle.9 
 |-  ( ph -> R e. RR* )
8 lmle.10 
 |-  ( ( ph /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )
9 2 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
10 3 9 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
11 lmrel 
 |-  Rel ( ~~>t ` J )
12 releldm 
 |-  ( ( Rel ( ~~>t ` J ) /\ F ( ~~>t ` J ) P ) -> F e. dom ( ~~>t ` J ) )
13 11 5 12 sylancr 
 |-  ( ph -> F e. dom ( ~~>t ` J ) )
14 1 10 4 13 lmff 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )
15 eqid 
 |-  ( ZZ>= ` j ) = ( ZZ>= ` j )
16 10 adantr 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> J e. ( TopOn ` X ) )
17 simprl 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> j e. Z )
18 17 1 eleqtrdi 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> j e. ( ZZ>= ` M ) )
19 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
20 18 19 syl 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> j e. ZZ )
21 5 adantr 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> F ( ~~>t ` J ) P )
22 oveq2 
 |-  ( x = ( F ` k ) -> ( Q D x ) = ( Q D ( F ` k ) ) )
23 22 breq1d 
 |-  ( x = ( F ` k ) -> ( ( Q D x ) <_ R <-> ( Q D ( F ` k ) ) <_ R ) )
24 fvres 
 |-  ( k e. ( ZZ>= ` j ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) = ( F ` k ) )
25 24 adantl 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) = ( F ` k ) )
26 simprr 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )
27 26 ffvelcdmda 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) e. X )
28 25 27 eqeltrrd 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )
29 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
30 17 29 sylan 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
31 8 adantlr 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )
32 30 31 syldan 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( Q D ( F ` k ) ) <_ R )
33 23 28 32 elrabd 
 |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. { x e. X | ( Q D x ) <_ R } )
34 eqid 
 |-  { x e. X | ( Q D x ) <_ R } = { x e. X | ( Q D x ) <_ R }
35 2 34 blcld 
 |-  ( ( D e. ( *Met ` X ) /\ Q e. X /\ R e. RR* ) -> { x e. X | ( Q D x ) <_ R } e. ( Clsd ` J ) )
36 3 6 7 35 syl3anc 
 |-  ( ph -> { x e. X | ( Q D x ) <_ R } e. ( Clsd ` J ) )
37 36 adantr 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> { x e. X | ( Q D x ) <_ R } e. ( Clsd ` J ) )
38 15 16 20 21 33 37 lmcld 
 |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> P e. { x e. X | ( Q D x ) <_ R } )
39 14 38 rexlimddv 
 |-  ( ph -> P e. { x e. X | ( Q D x ) <_ R } )
40 oveq2 
 |-  ( x = P -> ( Q D x ) = ( Q D P ) )
41 40 breq1d 
 |-  ( x = P -> ( ( Q D x ) <_ R <-> ( Q D P ) <_ R ) )
42 41 elrab 
 |-  ( P e. { x e. X | ( Q D x ) <_ R } <-> ( P e. X /\ ( Q D P ) <_ R ) )
43 42 simprbi 
 |-  ( P e. { x e. X | ( Q D x ) <_ R } -> ( Q D P ) <_ R )
44 39 43 syl 
 |-  ( ph -> ( Q D P ) <_ R )