Metamath Proof Explorer

Theorem iscau

Description: Express the property " F is a Cauchy sequence of metric D ". Part of Definition 1.4-3 of Kreyszig p. 28. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion iscau 
|- ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. k e. ZZ ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) ) )

Proof

Step Hyp Ref Expression
1 caufval 
 |-  ( D e. ( *Met ` X ) -> ( Cau ` D ) = { f e. ( X ^pm CC ) | A. x e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) } )
2 1 eleq2d 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> F e. { f e. ( X ^pm CC ) | A. x e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) } ) )
3 reseq1 
 |-  ( f = F -> ( f |` ( ZZ>= ` k ) ) = ( F |` ( ZZ>= ` k ) ) )
4 eqidd 
 |-  ( f = F -> ( ZZ>= ` k ) = ( ZZ>= ` k ) )
5 fveq1 
 |-  ( f = F -> ( f ` k ) = ( F ` k ) )
6 5 oveq1d 
 |-  ( f = F -> ( ( f ` k ) ( ball ` D ) x ) = ( ( F ` k ) ( ball ` D ) x ) )
7 3 4 6 feq123d 
 |-  ( f = F -> ( ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) <-> ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) )
8 7 rexbidv 
 |-  ( f = F -> ( E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) <-> E. k e. ZZ ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) )
9 8 ralbidv 
 |-  ( f = F -> ( A. x e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) <-> A. x e. RR+ E. k e. ZZ ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) )
10 9 elrab 
 |-  ( F e. { f e. ( X ^pm CC ) | A. x e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) } <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. k e. ZZ ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) )
11 2 10 bitrdi 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. k e. ZZ ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) ) )