Definition df-cmet 19261

Description: Define the class of complete metrics. (Contributed by Mario Carneiro, 1-May-2014.)

Assertion

Ref	Expression
df-cmet

Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cmet

Step	Hyp	Ref	Expression
1		cms 19258	. 2
2		vx	. . 3
3		cvv 2965	. . 3
4		vd	. . . . . . . . 9
5	4	cv 1653	. . . . . . . 8
6		cmopn 16742	. . . . . . . 8
7	5, 6	cfv 5501	. . . . . . 7
8		vf	. . . . . . . 8
9	8	cv 1653	. . . . . . 7
10		cflim 18017	. . . . . . 7
11	7, 9, 10	co 6129	. . . . . 6
12		c0 3616	. . . . . 6
13	11, 12	wne 2606	. . . . 5
14		ccfil 19256	. . . . . 6
15	5, 14	cfv 5501	. . . . 5
16	13, 8, 15	wral 2712	. . . 4
17	2	cv 1653	. . . . 5
18		cme 16738	. . . . 5
19	17, 18	cfv 5501	. . . 4
20	16, 4, 19	crab 2716	. . 3
21	2, 3, 20	cmpt 4301	. 2
22	1, 21	wceq 1654	1

This definition is referenced by:  iscmet  19288