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

Definition df-cau 19082
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 19079 . 2  class  Cau
2 vd . . 3  set  d
3 cxmt 16614 . . . . 5  class  * Met
43crn 4821 . . . 4  class  ran  * Met
54cuni 3959 . . 3  class  U. ran  * Met
6 vj . . . . . . . . 9  set  j
76cv 1648 . . . . . . . 8  class  j
8 cuz 10422 . . . . . . . 8  class  ZZ>=
97, 8cfv 5396 . . . . . . 7  class  ( ZZ>= `  j )
10 vf . . . . . . . . . 10  set  f
1110cv 1648 . . . . . . . . 9  class  f
127, 11cfv 5396 . . . . . . . 8  class  ( f `
 j )
13 vx . . . . . . . . 9  set  x
1413cv 1648 . . . . . . . 8  class  x
152cv 1648 . . . . . . . . 9  class  d
16 cbl 16616 . . . . . . . . 9  class  ball
1715, 16cfv 5396 . . . . . . . 8  class  ( ball `  d )
1812, 14, 17co 6022 . . . . . . 7  class  ( ( f `  j ) ( ball `  d
) x )
1911, 9cres 4822 . . . . . . 7  class  ( f  |`  ( ZZ>= `  j )
)
209, 18, 19wf 5392 . . . . . 6  wff  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
21 cz 10216 . . . . . 6  class  ZZ
2220, 6, 21wrex 2652 . . . . 5  wff  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
23 crp 10546 . . . . 5  class  RR+
2422, 13, 23wral 2651 . . . 4  wff  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
2515cdm 4820 . . . . . 6  class  dom  d
2625cdm 4820 . . . . 5  class  dom  dom  d
27 cc 8923 . . . . 5  class  CC
28 cpm 6957 . . . . 5  class  ^pm
2926, 27, 28co 6022 . . . 4  class  ( dom 
dom  d  ^pm  CC )
3024, 10, 29crab 2655 . . 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 4209 . 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 1649 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  19101
  Copyright terms: Public domain W3C validator