MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cau Unicode version

Definition df-cau 18684
Description: Define a function on metric spaces whose value is the set of Cauchy sequences of the space. (Contributed by NM, 8-Sep-2006.)
Assertion
Ref Expression
df-cau  |-  Cau  =  ( d  e.  U. ran  * Met  |->  { f  e.  ( dom  dom  d  ^pm  CC )  | 
A. x  e.  RR+  E. j  e.  ZZ  (
f  |`  ( ZZ>= `  j
) ) : (
ZZ>= `  j ) --> ( ( f `  j
) ( ball `  d
) x ) } )
Distinct variable group:    f, d, j, x

Detailed syntax breakdown of Definition df-cau
StepHypRef Expression
1 cca 18681 . 2  class  Cau
2 vd . . 3  set  d
3 cxmt 16371 . . . . 5  class  * Met
43crn 4692 . . . 4  class  ran  * Met
54cuni 3829 . . 3  class  U. ran  * Met
6 vj . . . . . . . . 9  set  j
76cv 1624 . . . . . . . 8  class  j
8 cuz 10232 . . . . . . . 8  class  ZZ>=
97, 8cfv 5257 . . . . . . 7  class  ( ZZ>= `  j )
10 vf . . . . . . . . . 10  set  f
1110cv 1624 . . . . . . . . 9  class  f
127, 11cfv 5257 . . . . . . . 8  class  ( f `
 j )
13 vx . . . . . . . . 9  set  x
1413cv 1624 . . . . . . . 8  class  x
152cv 1624 . . . . . . . . 9  class  d
16 cbl 16373 . . . . . . . . 9  class  ball
1715, 16cfv 5257 . . . . . . . 8  class  ( ball `  d )
1812, 14, 17co 5860 . . . . . . 7  class  ( ( f `  j ) ( ball `  d
) x )
1911, 9cres 4693 . . . . . . 7  class  ( f  |`  ( ZZ>= `  j )
)
209, 18, 19wf 5253 . . . . . 6  wff  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
21 cz 10026 . . . . . 6  class  ZZ
2220, 6, 21wrex 2546 . . . . 5  wff  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
23 crp 10356 . . . . 5  class  RR+
2422, 13, 23wral 2545 . . . 4  wff  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
2515cdm 4691 . . . . . 6  class  dom  d
2625cdm 4691 . . . . 5  class  dom  dom  d
27 cc 8737 . . . . 5  class  CC
28 cpm 6775 . . . . 5  class  ^pm
2926, 27, 28co 5860 . . . 4  class  ( dom 
dom  d  ^pm  CC )
3024, 10, 29crab 2549 . . 3  class  { f  e.  ( dom  dom  d  ^pm  CC )  | 
A. x  e.  RR+  E. j  e.  ZZ  (
f  |`  ( ZZ>= `  j
) ) : (
ZZ>= `  j ) --> ( ( f `  j
) ( ball `  d
) x ) }
312, 5, 30cmpt 4079 . 2  class  ( d  e.  U. ran  * Met  |->  { f  e.  ( dom  dom  d  ^pm  CC )  |  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x ) } )
321, 31wceq 1625 1  wff  Cau  =  ( d  e.  U. ran  * Met  |->  { f  e.  ( dom  dom  d  ^pm  CC )  | 
A. x  e.  RR+  E. j  e.  ZZ  (
f  |`  ( ZZ>= `  j
) ) : (
ZZ>= `  j ) --> ( ( f `  j
) ( ball `  d
) x ) } )
Colors of variables: wff set class
This definition is referenced by:  caufval  18703
  Copyright terms: Public domain W3C validator