Definition df-cmet 23055

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

Assertion

Ref	Expression
df-cmet	|- CMet = ( x e. _V |-> { d e. ( Met ` x ) | A. f e. (CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )

Distinct variable group:   f, d, x

Detailed syntax breakdown of Definition df-cmet

Step	Hyp	Ref	Expression
1		cms 23052	. 2 class CMet
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vd	. . . . . . . . 9 setvar d
5	4	cv 1482	. . . . . . . 8 class d
6		cmopn 19736	. . . . . . . 8 class MetOpen
7	5, 6	cfv 5888	. . . . . . 7 class ( MetOpen ` d )
8		vf	. . . . . . . 8 setvar f
9	8	cv 1482	. . . . . . 7 class f
10		cflim 21738	. . . . . . 7 class fLim
11	7, 9, 10	co 6650	. . . . . 6 class ( ( MetOpen ` d ) fLim f )
12		c0 3915	. . . . . 6 class (/)
13	11, 12	wne 2794	. . . . 5 wff ( ( MetOpen ` d ) fLim f ) =/= (/)
14		ccfil 23050	. . . . . 6 class CauFil
15	5, 14	cfv 5888	. . . . 5 class (CauFil ` d )
16	13, 8, 15	wral 2912	. . . 4 wff A. f e. (CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/)
17	2	cv 1482	. . . . 5 class x
18		cme 19732	. . . . 5 class Met
19	17, 18	cfv 5888	. . . 4 class ( Met ` x )
20	16, 4, 19	crab 2916	. . 3 class { d e. ( Met ` x ) | A. f e. (CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) }
21	2, 3, 20	cmpt 4729	. 2 class ( x e. _V |-> { d e. ( Met ` x ) | A. f e. (CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )
22	1, 21	wceq 1483	1 wff CMet = ( x e. _V |-> { d e. ( Met ` x ) | A. f e. (CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )

This definition is referenced by:  iscmet  23082