Theorem blssopn

Description: The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypothesis	mopni.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
Assertion	blssopn	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ran}\mathrm{ball}\left(D\right)\subseteq J$$

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
2		blbas	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ran}\mathrm{ball}\left(D\right)\in \mathrm{TopBases}$$
3		bastg	$$⊢\mathrm{ran}\mathrm{ball}\left(D\right)\in \mathrm{TopBases}\to \mathrm{ran}\mathrm{ball}\left(D\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$
4	2 3	syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ran}\mathrm{ball}\left(D\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$
5	1	mopnval	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$
6	4 5	sseqtrrd	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ran}\mathrm{ball}\left(D\right)\subseteq J$$