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)$$