Definition df-cmet 19714

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 19711	. 2
2		vx	. . 3
3		cvv 3006	. . 3
4		vd	. . . . . . . . 9
5	4	cv 1661	. . . . . . . 8
6		cmopn 17194	. . . . . . . 8
7	5, 6	cfv 5417	. . . . . . 7
8		vf	. . . . . . . 8
9	8	cv 1661	. . . . . . 7
10		cflim 18470	. . . . . . 7
11	7, 9, 10	co 6067	. . . . . 6
12		c0 3660	. . . . . 6
13	11, 12	wne 2644	. . . . 5
14		ccfil 19709	. . . . . 6
15	5, 14	cfv 5417	. . . . 5
16	13, 8, 15	wral 2751	. . . 4
17	2	cv 1661	. . . . 5
18		cme 17190	. . . . 5
19	17, 18	cfv 5417	. . . 4
20	16, 4, 19	crab 2755	. . 3
21	2, 3, 20	cmpt 4360	. 2
22	1, 21	wceq 1662	1

This definition is referenced by:  iscmet  19741