Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmetu 
 |-  metUnif
1 vd 
 |-  d
2 cpsmet 
 |-  PsMet
3 2 crn 
 |-  ran PsMet
4 3 cuni 
 |-  U. ran PsMet
5 1 cv 
 |-  d
6 5 cdm 
 |-  dom d
7 6 cdm 
 |-  dom dom d
8 7 7 cxp 
 |-  ( dom dom d X. dom dom d )
9 cfg 
 |-  filGen
10 va 
 |-  a
11 crp 
 |-  RR+
12 5 ccnv 
 |-  `' d
13 cc0 
 |-  0
14 cico 
 |-  [,)
15 10 cv 
 |-  a
16 13 15 14 co 
 |-  ( 0 [,) a )
17 12 16 cima 
 |-  ( `' d " ( 0 [,) a ) )
18 10 11 17 cmpt 
 |-  ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) )
19 18 crn 
 |-  ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) )
20 8 19 9 co 
 |-  ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) )
21 1 4 20 cmpt 
 |-  ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
22 0 21 wceq 
 |-  metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )