Definition df-cmet

Description: Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014)

	Ref	Expression
Assertion	df-cmet	$$⊢\mathrm{CMet}=\left(x\in \mathrm{V}⟼\left\{d\in \mathrm{Met}\left(x\right)|\forall f\in \mathrm{CauFil}\left(d\right)\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\ne \varnothing \right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmet	$$class\mathrm{CMet}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vd	$$setvard$$
4		cmet	$$class\mathrm{Met}$$
5	1	cv	$$setvarx$$
6	5 4	cfv	$$class\mathrm{Met}\left(x\right)$$
7		vf	$$setvarf$$
8		ccfil	$$class\mathrm{CauFil}$$
9	3	cv	$$setvard$$
10	9 8	cfv	$$class\mathrm{CauFil}\left(d\right)$$
11		cmopn	$$class\mathrm{MetOpen}$$
12	9 11	cfv	$$class\mathrm{MetOpen}\left(d\right)$$
13		cflim	$$class\mathrm{fLim}$$
14	7	cv	$$setvarf$$
15	12 14 13	co	$$class\left(\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\right)$$
16		c0	$$class\varnothing$$
17	15 16	wne	$$wff\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\ne \varnothing$$
18	17 7 10	wral	$$wff\forall f\in \mathrm{CauFil}\left(d\right)\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\ne \varnothing$$
19	18 3 6	crab	$$class\left\{d\in \mathrm{Met}\left(x\right)|\forall f\in \mathrm{CauFil}\left(d\right)\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\ne \varnothing \right\}$$
20	1 2 19	cmpt	$$class\left(x\in \mathrm{V}⟼\left\{d\in \mathrm{Met}\left(x\right)|\forall f\in \mathrm{CauFil}\left(d\right)\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\ne \varnothing \right\}\right)$$
21	0 20	wceq	$$wff\mathrm{CMet}=\left(x\in \mathrm{V}⟼\left\{d\in \mathrm{Met}\left(x\right)|\forall f\in \mathrm{CauFil}\left(d\right)\mathrm{MetOpen}\left(d\right)\mathrm{fLim}f\ne \varnothing \right\}\right)$$