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 ‘ 𝑋 ) ) |