Definition df-metu

Description: Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Assertion	df-metu	$$⊢\mathrm{metUnif}=\left(d\in \bigcup \mathrm{ran}\mathrm{PsMet}⟼\left(\mathrm{dom}\mathrm{dom}d\times \mathrm{dom}\mathrm{dom}d\right)\mathrm{filGen}\mathrm{ran}\left(a\in {ℝ}^{+}⟼d^{-1}\left[\left[0,a\right)\right]\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmetu	$$class\mathrm{metUnif}$$
1		vd	$$setvard$$
2		cpsmet	$$class\mathrm{PsMet}$$
3	2	crn	$$class\mathrm{ran}\mathrm{PsMet}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{PsMet}$$
5	1	cv	$$setvard$$
6	5	cdm	$$class\mathrm{dom}d$$
7	6	cdm	$$class\mathrm{dom}\mathrm{dom}d$$
8	7 7	cxp	$$class\left(\mathrm{dom}\mathrm{dom}d\times \mathrm{dom}\mathrm{dom}d\right)$$
9		cfg	$$class\mathrm{filGen}$$
10		va	$$setvara$$
11		crp	$$class{ℝ}^{+}$$
12	5	ccnv	$$class{d}^{-1}$$
13		cc0	$$class0$$
14		cico	$$class\left[.\right)$$
15	10	cv	$$setvara$$
16	13 15 14	co	$$class\left[0,a\right)$$
17	12 16	cima	$$class{d}^{-1}\left[\left[0,a\right)\right]$$
18	10 11 17	cmpt	$$class\left(a\in {ℝ}^{+}⟼d^{-1}\left[\left[0,a\right)\right]\right)$$
19	18	crn	$$class\mathrm{ran}\left(a\in {ℝ}^{+}⟼d^{-1}\left[\left[0,a\right)\right]\right)$$
20	8 19 9	co	$$class\left(\left(\mathrm{dom}\mathrm{dom}d\times \mathrm{dom}\mathrm{dom}d\right)\mathrm{filGen}\mathrm{ran}\left(a\in {ℝ}^{+}⟼d^{-1}\left[\left[0,a\right)\right]\right)\right)$$
21	1 4 20	cmpt	$$class\left(d\in \bigcup \mathrm{ran}\mathrm{PsMet}⟼\left(\mathrm{dom}\mathrm{dom}d\times \mathrm{dom}\mathrm{dom}d\right)\mathrm{filGen}\mathrm{ran}\left(a\in {ℝ}^{+}⟼d^{-1}\left[\left[0,a\right)\right]\right)\right)$$
22	0 21	wceq	$$wff\mathrm{metUnif}=\left(d\in \bigcup \mathrm{ran}\mathrm{PsMet}⟼\left(\mathrm{dom}\mathrm{dom}d\times \mathrm{dom}\mathrm{dom}d\right)\mathrm{filGen}\mathrm{ran}\left(a\in {ℝ}^{+}⟼d^{-1}\left[\left[0,a\right)\right]\right)\right)$$