Step |
Hyp |
Ref |
Expression |
1 |
|
xmetpsmet |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) |
2 |
|
psmetutop |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
3 |
1 2
|
sylan2 |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
4 |
|
eqid |
⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 ) |
5 |
4
|
mopnval |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
7 |
3 6
|
eqtr4d |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) ) |