This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ⋃ ran ⁡ PsMet ⟼ dom ⁡ dom ⁡ d × dom ⁡ dom ⁡ d filGen ran ⁡ a ∈ ℝ + ⟼ d -1 0 a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmetu class metUnif
1 vd setvar d
2 cpsmet class PsMet
3 2 crn class ran ⁡ PsMet
4 3 cuni class ⋃ ran ⁡ PsMet
5 1 cv setvar d
6 5 cdm class dom ⁡ d
7 6 cdm class dom ⁡ dom ⁡ d
8 7 7 cxp class dom ⁡ dom ⁡ d × dom ⁡ dom ⁡ d
9 cfg class filGen
10 va setvar a
11 crp class ℝ +
12 5 ccnv class d -1
13 cc0 class 0
14 cico class .
15 10 cv setvar a
16 13 15 14 co class 0 a
17 12 16 cima class d -1 0 a
18 10 11 17 cmpt class a ∈ ℝ + ⟼ d -1 0 a
19 18 crn class ran ⁡ a ∈ ℝ + ⟼ d -1 0 a
20 8 19 9 co class dom ⁡ dom ⁡ d × dom ⁡ dom ⁡ d filGen ran ⁡ a ∈ ℝ + ⟼ d -1 0 a
21 1 4 20 cmpt class d ∈ ⋃ ran ⁡ PsMet ⟼ dom ⁡ dom ⁡ d × dom ⁡ dom ⁡ d filGen ran ⁡ a ∈ ℝ + ⟼ d -1 0 a
22 0 21 wceq wff metUnif = d ∈ ⋃ ran ⁡ PsMet ⟼ dom ⁡ dom ⁡ d × dom ⁡ dom ⁡ d filGen ran ⁡ a ∈ ℝ + ⟼ d -1 0 a