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

Definition df-cau 20772
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 20769 . 2  class  Cau
2 vd . . 3  setvar  d
3 cxmt 17806 . . . . 5  class  *Met
43crn 4846 . . . 4  class  ran  *Met
54cuni 4096 . . 3  class  U. ran  *Met
6 vj . . . . . . . . 9  setvar  j
76cv 1368 . . . . . . . 8  class  j
8 cuz 10866 . . . . . . . 8  class  ZZ>=
97, 8cfv 5423 . . . . . . 7  class  ( ZZ>= `  j )
10 vf . . . . . . . . . 10  setvar  f
1110cv 1368 . . . . . . . . 9  class  f
127, 11cfv 5423 . . . . . . . 8  class  ( f `
 j )
13 vx . . . . . . . . 9  setvar  x
1413cv 1368 . . . . . . . 8  class  x
152cv 1368 . . . . . . . . 9  class  d
16 cbl 17808 . . . . . . . . 9  class  ball
1715, 16cfv 5423 . . . . . . . 8  class  ( ball `  d )
1812, 14, 17co 6096 . . . . . . 7  class  ( ( f `  j ) ( ball `  d
) x )
1911, 9cres 4847 . . . . . . 7  class  ( f  |`  ( ZZ>= `  j )
)
209, 18, 19wf 5419 . . . . . 6  wff  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
21 cz 10651 . . . . . 6  class  ZZ
2220, 6, 21wrex 2721 . . . . 5  wff  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
23 crp 10996 . . . . 5  class  RR+
2422, 13, 23wral 2720 . . . 4  wff  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( f `  j ) ( ball `  d
) x )
2515cdm 4845 . . . . . 6  class  dom  d
2625cdm 4845 . . . . 5  class  dom  dom  d
27 cc 9285 . . . . 5  class  CC
28 cpm 7220 . . . . 5  class  ^pm
2926, 27, 28co 6096 . . . 4  class  ( dom 
dom  d  ^pm  CC )
3024, 10, 29crab 2724 . . 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 4355 . 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 1369 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 setvar class
This definition is referenced by:  caufval  20791
  Copyright terms: Public domain W3C validator