Metamath Proof Explorer

Theorem lmcau

Description: Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of Kreyszig p. 28. (Contributed by NM, 29-Jan-2008) (Proof shortened by Mario Carneiro, 5-May-2014)

Ref Expression
Hypothesis lmcau.1 
|- J = ( MetOpen ` D )
Assertion lmcau 
|- ( D e. ( *Met ` X ) -> dom ( ~~>t ` J ) C_ ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 lmcau.1 
 |-  J = ( MetOpen ` D )
2 1 methaus 
 |-  ( D e. ( *Met ` X ) -> J e. Haus )
3 lmfun 
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )
4 funfvbrb 
 |-  ( Fun ( ~~>t ` J ) -> ( f e. dom ( ~~>t ` J ) <-> f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) )
5 2 3 4 3syl 
 |-  ( D e. ( *Met ` X ) -> ( f e. dom ( ~~>t ` J ) <-> f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) )
6 id 
 |-  ( D e. ( *Met ` X ) -> D e. ( *Met ` X ) )
7 1 6 lmmbr 
 |-  ( D e. ( *Met ` X ) -> ( f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) <-> ( f e. ( X ^pm CC ) /\ ( ( ~~>t ` J ) ` f ) e. X /\ A. y e. RR+ E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) ) ) )
8 7 biimpa 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> ( f e. ( X ^pm CC ) /\ ( ( ~~>t ` J ) ` f ) e. X /\ A. y e. RR+ E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) ) )
9 8 simp1d 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> f e. ( X ^pm CC ) )
10 simprr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
11 simplll 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> D e. ( *Met ` X ) )
12 8 simp2d 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> ( ( ~~>t ` J ) ` f ) e. X )
13 12 ad2antrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( ( ~~>t ` J ) ` f ) e. X )
14 rpre 
 |-  ( x e. RR+ -> x e. RR )
15 14 ad2antlr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> x e. RR )
16 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
17 16 ad2antrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> j e. ( ZZ>= ` j ) )
18 17 fvresd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( ( f |` ( ZZ>= ` j ) ) ` j ) = ( f ` j ) )
19 10 17 ffvelcdmd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( ( f |` ( ZZ>= ` j ) ) ` j ) e. ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
20 18 19 eqeltrrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( f ` j ) e. ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
21 blhalf 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( ( ~~>t ` J ) ` f ) e. X ) /\ ( x e. RR /\ ( f ` j ) e. ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) C_ ( ( f ` j ) ( ball ` D ) x ) )
22 11 13 15 20 21 syl22anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) C_ ( ( f ` j ) ( ball ` D ) x ) )
23 10 22 fssd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) /\ ( j e. ZZ /\ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` D ) x ) )
24 rphalfcl 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
25 8 simp3d 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> A. y e. RR+ E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) )
26 oveq2 
 |-  ( y = ( x / 2 ) -> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) = ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
27 26 feq3d 
 |-  ( y = ( x / 2 ) -> ( ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) <-> ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) )
28 27 rexbidv 
 |-  ( y = ( x / 2 ) -> ( E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) <-> E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) )
29 28 rspcv 
 |-  ( ( x / 2 ) e. RR+ -> ( A. y e. RR+ E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) y ) -> E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) )
30 24 25 29 syl2im 
 |-  ( x e. RR+ -> ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) )
31 30 impcom 
 |-  ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) -> E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
32 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
33 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
34 reseq2 
 |-  ( u = ( ZZ>= ` j ) -> ( f |` u ) = ( f |` ( ZZ>= ` j ) ) )
35 id 
 |-  ( u = ( ZZ>= ` j ) -> u = ( ZZ>= ` j ) )
36 34 35 feq12d 
 |-  ( u = ( ZZ>= ` j ) -> ( ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) <-> ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) )
37 36 rexrn 
 |-  ( ZZ>= Fn ZZ -> ( E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) <-> E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) ) )
38 32 33 37 mp2b 
 |-  ( E. u e. ran ZZ>= ( f |` u ) : u --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) <-> E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
39 31 38 sylib 
 |-  ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) -> E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( ( ~~>t ` J ) ` f ) ( ball ` D ) ( x / 2 ) ) )
40 23 39 reximddv 
 |-  ( ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) /\ x e. RR+ ) -> E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` D ) x ) )
41 40 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` D ) x ) )
42 iscau 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( Cau ` D ) <-> ( f e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` D ) x ) ) ) )
43 42 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> ( f e. ( Cau ` D ) <-> ( f e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` D ) x ) ) ) )
44 9 41 43 mpbir2and 
 |-  ( ( D e. ( *Met ` X ) /\ f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) ) -> f e. ( Cau ` D ) )
45 44 ex 
 |-  ( D e. ( *Met ` X ) -> ( f ( ~~>t ` J ) ( ( ~~>t ` J ) ` f ) -> f e. ( Cau ` D ) ) )
46 5 45 sylbid 
 |-  ( D e. ( *Met ` X ) -> ( f e. dom ( ~~>t ` J ) -> f e. ( Cau ` D ) ) )
47 46 ssrdv 
 |-  ( D e. ( *Met ` X ) -> dom ( ~~>t ` J ) C_ ( Cau ` D ) )