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

Definition df-cau 18682
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 18679 . 2  class  Cau
2 vd . . 3  set  d
3 cxmt 16369 . . . . 5  class  * Met
43crn 4690 . . . 4  class  ran  * Met
54cuni 3827 . . 3  class  U. ran  * Met
6 vj . . . . . . . . 9  set  j
76cv 1622 . . . . . . . 8  class  j
8 cuz 10230 . . . . . . . 8  class  ZZ>=
97, 8cfv 5255 . . . . . . 7  class  ( ZZ>= `  j )
10 vf . . . . . . . . . 10  set  f
1110cv 1622 . . . . . . . . 9  class  f
127, 11cfv 5255 . . . . . . . 8  class  ( f `
 j )
13 vx . . . . . . . . 9  set  x
1413cv 1622 . . . . . . . 8  class  x
152cv 1622 . . . . . . . . 9  class  d
16 cbl 16371 . . . . . . . . 9  class  ball
1715, 16cfv 5255 . . . . . . . 8  class  ( ball `  d )
1812, 14, 17co 5858 . . . . . . 7  class  ( ( f `  j ) ( ball `  d
) x )
1911, 9cres 4691 . . . . . . 7  class  ( f  |`  ( ZZ>= `  j )
)
209, 18, 19wf 5251 . . . . . 6  wff  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
21 cz 10024 . . . . . 6  class  ZZ
2220, 6, 21wrex 2544 . . . . 5  wff  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
23 crp 10354 . . . . 5  class  RR+
2422, 13, 23wral 2543 . . . 4  wff  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
2515cdm 4689 . . . . . 6  class  dom  d
2625cdm 4689 . . . . 5  class  dom  dom  d
27 cc 8735 . . . . 5  class  CC
28 cpm 6773 . . . . 5  class  ^pm
2926, 27, 28co 5858 . . . 4  class  ( dom 
dom  d  ^pm  CC )
3024, 10, 29crab 2547 . . 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 4077 . 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 1623 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  18701
  Copyright terms: Public domain W3C validator