Definition df-cmet 9202

Description: Define the class of complete metrics.

Assertion

Ref	Expression
df-cmet	|- CMet = {x e. Met | A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y}

Distinct variable group:   x,y,f

Detailed syntax breakdown of Definition df-cmet

Step	Hyp	Ref	Expression
1		cms 9199	. 2 class CMet
2		vf	. . . . . . 7 set f
3	2	cv 1297	. . . . . 6 class f
4		vy	. . . . . . 7 set y
5	4	cv 1297	. . . . . 6 class y
6		vx	. . . . . . . 8 set x
7	6	cv 1297	. . . . . . 7 class x
8		clm 9197	. . . . . . 7 class ~~>m
9	7, 8	cfv 3998	. . . . . 6 class (~~>m` x)
10	3, 5, 9	wbr 3338	. . . . 5 wff f(~~>m` x)y
11	7	cdm 3986	. . . . . 6 class dom x
12	11	cdm 3986	. . . . 5 class dom dom x
13	10, 4, 12	wrex 2106	. . . 4 wff E.y e. dom dom x f(~~>m` x)y
14		cca 9198	. . . . 5 class Cau
15	7, 14	cfv 3998	. . . 4 class (Cau` x)
16	13, 2, 15	wral 2105	. . 3 wff A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y
17		cme 9066	. . 3 class Met
18	16, 6, 17	crab 2108	. 2 class {x e. Met | A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y}
19	1, 18	wceq 1298	1 wff CMet = {x e. Met | A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y}

This definition is referenced by:  iscms 9224

Copyright terms: Public domain