# Metamath Proof Explorer

## Theorem mopntopon

Description: The set of open sets of a metric space X is a topology on X . Remark in Kreyszig p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis mopnval.1 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
Assertion mopntopon ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 mopnval.1 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 1 mopnval ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left({D}\right)\right)$
3 blbas ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{ran}\mathrm{ball}\left({D}\right)\in \mathrm{TopBases}$
4 tgtopon ${⊢}\mathrm{ran}\mathrm{ball}\left({D}\right)\in \mathrm{TopBases}\to \mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left({D}\right)\right)\in \mathrm{TopOn}\left(\bigcup \mathrm{ran}\mathrm{ball}\left({D}\right)\right)$
5 3 4 syl ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left({D}\right)\right)\in \mathrm{TopOn}\left(\bigcup \mathrm{ran}\mathrm{ball}\left({D}\right)\right)$
6 unirnbl ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \bigcup \mathrm{ran}\mathrm{ball}\left({D}\right)={X}$
7 6 fveq2d ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{TopOn}\left(\bigcup \mathrm{ran}\mathrm{ball}\left({D}\right)\right)=\mathrm{TopOn}\left({X}\right)$
8 5 7 eleqtrd ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left({D}\right)\right)\in \mathrm{TopOn}\left({X}\right)$
9 2 8 eqeltrd ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$