Definition df-cmet 20225

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 20222	. 2
2		vx	. . 3
3		cvv 3015	. . 3
4		vd	. . . . . . . . 9
5	4	cv 1669	. . . . . . . 8
6		cmopn 17316	. . . . . . . 8
7	5, 6	cfv 5438	. . . . . . 7
8		vf	. . . . . . . 8
9	8	cv 1669	. . . . . . 7
10		cflim 18981	. . . . . . 7
11	7, 9, 10	co 6103	. . . . . 6
12		c0 3673	. . . . . 6
13	11, 12	wne 2652	. . . . 5
14		ccfil 20220	. . . . . 6
15	5, 14	cfv 5438	. . . . 5
16	13, 8, 15	wral 2759	. . . 4
17	2	cv 1669	. . . . 5
18		cme 17312	. . . . 5
19	17, 18	cfv 5438	. . . 4
20	16, 4, 19	crab 2763	. . 3
21	2, 3, 20	cmpt 4376	. 2
22	1, 21	wceq 1670	1

This definition is referenced by:  iscmet  20252