Definition df-metu 14588

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 = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )

Distinct variable group:   a, d

Detailed syntax breakdown of Definition df-metu

Step	Hyp	Ref	Expression
1		cmetu 14580	. 2 class metUnif
2		vd	. . 3 setvar d
3		cpsmet 14573	. . . . 5 class PsMet
4	3	crn 4728	. . . 4 class ran PsMet
5	4	cuni 3894	. . 3 class U. ran PsMet
6	2	cv 1396	. . . . . . 7 class d
7	6	cdm 4727	. . . . . 6 class dom d
8	7	cdm 4727	. . . . 5 class dom dom d
9	8, 8	cxp 4725	. . . 4 class ( dom dom d X. dom dom d )
10		va	. . . . . 6 setvar a
11		crp 9893	. . . . . 6 class RR+
12	6	ccnv 4726	. . . . . . 7 class `' d
13		cc0 8037	. . . . . . . 8 class 0
14	10	cv 1396	. . . . . . . 8 class a
15		cico 10130	. . . . . . . 8 class [,)
16	13, 14, 15	co 6023	. . . . . . 7 class ( 0 [,) a )
17	12, 16	cima 4730	. . . . . 6 class ( `' d " ( 0 [,) a ) )
18	10, 11, 17	cmpt 4151	. . . . 5 class ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) )
19	18	crn 4728	. . . 4 class ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) )
20		cfg 14578	. . . 4 class filGen
21	9, 19, 20	co 6023	. . 3 class ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) )
22	2, 5, 21	cmpt 4151	. 2 class ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
23	1, 22	wceq 1397	1 wff metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )

This definition is referenced by:  metuex  14593