Definition df-cmet 7924

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 7921	. 2 class CMet
2		vf	. . . . . . 7 set f
3	2	cv 955	. . . . . 6 class f
4		vy	. . . . . . 7 set y
5	4	cv 955	. . . . . 6 class y
6		vx	. . . . . . . 8 set x
7	6	cv 955	. . . . . . 7 class x
8		clm 7919	. . . . . . 7 class ~~>m
9	7, 8	cfv 3182	. . . . . 6 class (~~>m` x)
10	3, 5, 9	wbr 2619	. . . . 5 wff f(~~>m` x)y
11	7	cdm 3170	. . . . . 6 class dom x
12	11	cdm 3170	. . . . 5 class dom dom x
13	10, 4, 12	wrex 1646	. . . 4 wff E.y e. dom dom x f(~~>m` x)y
14		cca 7920	. . . . 5 class Cau
15	7, 14	cfv 3182	. . . 4 class (Cau` x)
16	13, 2, 15	wral 1645	. . 3 wff A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y
17		cme 7789	. . 3 class Met
18	16, 6, 17	crab 1648	. 2 class {x e. Met | A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y}
19	1, 18	wceq 956	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 7946

Copyright terms: Public domain