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
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cau
StepHypRef Expression
1 cca 19237 . 2
2 vd . . 3
3 cxmt 16717 . . . . 5
43crn 4908 . . . 4
54cuni 4039 . . 3
6 vj . . . . . . . . 9
76cv 1652 . . . . . . . 8
8 cuz 10519 . . . . . . . 8
97, 8cfv 5483 . . . . . . 7
10 vf . . . . . . . . . 10
1110cv 1652 . . . . . . . . 9
127, 11cfv 5483 . . . . . . . 8
13 vx . . . . . . . . 9
1413cv 1652 . . . . . . . 8
152cv 1652 . . . . . . . . 9
16 cbl 16719 . . . . . . . . 9
1715, 16cfv 5483 . . . . . . . 8
1812, 14, 17co 6110 . . . . . . 7
1911, 9cres 4909 . . . . . . 7
209, 18, 19wf 5479 . . . . . 6
21 cz 10313 . . . . . 6
2220, 6, 21wrex 2712 . . . . 5
23 crp 10643 . . . . 5
2422, 13, 23wral 2711 . . . 4
2515cdm 4907 . . . . . 6
2625cdm 4907 . . . . 5
27 cc 9019 . . . . 5
28 cpm 7048 . . . . 5
2926, 27, 28co 6110 . . . 4
3024, 10, 29crab 2715 . . 3
312, 5, 30cmpt 4291 . 2
321, 31wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  caufval  19259
 Copyright terms: Public domain W3C validator