Definition df-metu 20218

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.)

Assertion

Ref	Expression
df-metu	⊢ metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))

Distinct variable group:   𝑎,𝑑

Detailed syntax breakdown of Definition df-metu

Step	Hyp	Ref	Expression
1		cmetu 20210	. 2 class metUnif
2		vd	. . 3 setvar 𝑑
3		cpsmet 20203	. . . . 5 class PsMet
4	3	crn 5526	. . . 4 class ran PsMet
5	4	cuni 4796	. . 3 class ∪ ran PsMet
6	2	cv 1541	. . . . . . 7 class 𝑑
7	6	cdm 5525	. . . . . 6 class dom 𝑑
8	7	cdm 5525	. . . . 5 class dom dom 𝑑
9	8, 8	cxp 5523	. . . 4 class (dom dom 𝑑 × dom dom 𝑑)
10		va	. . . . . 6 setvar 𝑎
11		crp 12474	. . . . . 6 class ℝ+
12	6	ccnv 5524	. . . . . . 7 class ◡𝑑
13		cc0 10617	. . . . . . . 8 class 0
14	10	cv 1541	. . . . . . . 8 class 𝑎
15		cico 12825	. . . . . . . 8 class [,)
16	13, 14, 15	co 7172	. . . . . . 7 class (0[,)𝑎)
17	12, 16	cima 5528	. . . . . 6 class (◡𝑑 “ (0[,)𝑎))
18	10, 11, 17	cmpt 5110	. . . . 5 class (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))
19	18	crn 5526	. . . 4 class ran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))
20		cfg 20208	. . . 4 class filGen
21	9, 19, 20	co 7172	. . 3 class ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))
22	2, 5, 21	cmpt 5110	. 2 class (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))
23	1, 22	wceq 1542	1 wff metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))

This definition is referenced by:  metuval  23304