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

Definition df-cau 19201
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
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-cau
StepHypRef Expression
1 cca 19198 . 2
2 vd . . 3
3 cxmt 16678 . . . . 5
43crn 4871 . . . 4
54cuni 4007 . . 3
6 vj . . . . . . . . 9
76cv 1651 . . . . . . . 8
8 cuz 10480 . . . . . . . 8
97, 8cfv 5446 . . . . . . 7
10 vf . . . . . . . . . 10
1110cv 1651 . . . . . . . . 9
127, 11cfv 5446 . . . . . . . 8
13 vx . . . . . . . . 9
1413cv 1651 . . . . . . . 8
152cv 1651 . . . . . . . . 9
16 cbl 16680 . . . . . . . . 9
1715, 16cfv 5446 . . . . . . . 8
1812, 14, 17co 6073 . . . . . . 7
1911, 9cres 4872 . . . . . . 7
209, 18, 19wf 5442 . . . . . 6
21 cz 10274 . . . . . 6
2220, 6, 21wrex 2698 . . . . 5
23 crp 10604 . . . . 5
2422, 13, 23wral 2697 . . . 4
2515cdm 4870 . . . . . 6
2625cdm 4870 . . . . 5
27 cc 8980 . . . . 5
28 cpm 7011 . . . . 5
2926, 27, 28co 6073 . . . 4
3024, 10, 29crab 2701 . . 3
312, 5, 30cmpt 4258 . 2
321, 31wceq 1652 1
Colors of variables: wff set class
This definition is referenced by:  caufval  19220
  Copyright terms: Public domain W3C validator