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 = ( 𝑑 ∈ ∪ ran PsMet ↦ ( ( dom dom 𝑑 × dom dom 𝑑 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmetu ⊢ metUnif
1 vd ⊢ 𝑑
2 cpsmet ⊢ PsMet
3 2 crn ⊢ ran PsMet
4 3 cuni ⊢ ∪ ran PsMet
5 1 cv ⊢ 𝑑
6 5 cdm ⊢ dom 𝑑
7 6 cdm ⊢ dom dom 𝑑
8 7 7 cxp ⊢ ( dom dom 𝑑 × dom dom 𝑑 )
9 cfg ⊢ filGen
10 va ⊢ 𝑎
11 crp ⊢ ℝ+
12 5 ccnv ⊢ ◡ 𝑑
13 cc0 ⊢ 0
14 cico ⊢ [,)
15 10 cv ⊢ 𝑎
16 13 15 14 co ⊢ ( 0 [,) 𝑎 )
17 12 16 cima ⊢ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) )
18 10 11 17 cmpt ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) )
19 18 crn ⊢ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) )
20 8 19 9 co ⊢ ( ( dom dom 𝑑 × dom dom 𝑑 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) )
21 1 4 20 cmpt ⊢ ( 𝑑 ∈ ∪ ran PsMet ↦ ( ( dom dom 𝑑 × dom dom 𝑑 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) ) )
22 0 21 wceq ⊢ metUnif = ( 𝑑 ∈ ∪ ran PsMet ↦ ( ( dom dom 𝑑 × dom dom 𝑑 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) ) )