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

Definition df-cmet 19215
 Description: Define the class of complete metrics. (Contributed by Mario Carneiro, 1-May-2014.)
Assertion
Ref Expression
df-cmet CauFil
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cmet
StepHypRef Expression
1 cms 19212 . 2
2 vx . . 3
3 cvv 2958 . . 3
4 vd . . . . . . . . 9
54cv 1652 . . . . . . . 8
6 cmopn 16696 . . . . . . . 8
75, 6cfv 5457 . . . . . . 7
8 vf . . . . . . . 8
98cv 1652 . . . . . . 7
10 cflim 17971 . . . . . . 7
117, 9, 10co 6084 . . . . . 6
12 c0 3630 . . . . . 6
1311, 12wne 2601 . . . . 5
14 ccfil 19210 . . . . . 6 CauFil
155, 14cfv 5457 . . . . 5 CauFil
1613, 8, 15wral 2707 . . . 4 CauFil
172cv 1652 . . . . 5
18 cme 16692 . . . . 5
1917, 18cfv 5457 . . . 4
2016, 4, 19crab 2711 . . 3 CauFil
212, 3, 20cmpt 4269 . 2 CauFil
221, 21wceq 1653 1 CauFil
 Colors of variables: wff set class This definition is referenced by:  iscmet  19242
 Copyright terms: Public domain W3C validator