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

Definition df-cau 19240
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 19237 . 2  class  Cau
2 vd . . 3  set  d
3 cxmt 16717 . . . . 5  class  * Met
43crn 4908 . . . 4  class  ran  * Met
54cuni 4039 . . 3  class  U. ran  * Met
6 vj . . . . . . . . 9  set  j
76cv 1652 . . . . . . . 8  class  j
8 cuz 10519 . . . . . . . 8  class  ZZ>=
97, 8cfv 5483 . . . . . . 7  class  ( ZZ>= `  j )
10 vf . . . . . . . . . 10  set  f
1110cv 1652 . . . . . . . . 9  class  f
127, 11cfv 5483 . . . . . . . 8  class  ( f `
 j )
13 vx . . . . . . . . 9  set  x
1413cv 1652 . . . . . . . 8  class  x
152cv 1652 . . . . . . . . 9  class  d
16 cbl 16719 . . . . . . . . 9  class  ball
1715, 16cfv 5483 . . . . . . . 8  class  ( ball `  d )
1812, 14, 17co 6110 . . . . . . 7  class  ( ( f `  j ) ( ball `  d
) x )
1911, 9cres 4909 . . . . . . 7  class  ( f  |`  ( ZZ>= `  j )
)
209, 18, 19wf 5479 . . . . . 6  wff  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
21 cz 10313 . . . . . 6  class  ZZ
2220, 6, 21wrex 2712 . . . . 5  wff  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
23 crp 10643 . . . . 5  class  RR+
2422, 13, 23wral 2711 . . . 4  wff  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
2515cdm 4907 . . . . . 6  class  dom  d
2625cdm 4907 . . . . 5  class  dom  dom  d
27 cc 9019 . . . . 5  class  CC
28 cpm 7048 . . . . 5  class  ^pm
2926, 27, 28co 6110 . . . 4  class  ( dom 
dom  d  ^pm  CC )
3024, 10, 29crab 2715 . . 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 4291 . 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 1653 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  19259
  Copyright terms: Public domain W3C validator