Metamath Proof Explorer


Theorem metuust

Description: The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion metuust ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 metuval ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
2 1 adantl ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
3 oveq2 ( 𝑎 = 𝑏 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑏 ) )
4 3 imaeq2d ( 𝑎 = 𝑏 → ( 𝐷 “ ( 0 [,) 𝑎 ) ) = ( 𝐷 “ ( 0 [,) 𝑏 ) ) )
5 4 cbvmptv ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑏 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑏 ) ) )
6 5 rneqi ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑏 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑏 ) ) )
7 6 metust ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∈ ( UnifOn ‘ 𝑋 ) )
8 2 7 eqeltrd ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )