Theorem mopnss

Description: An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006)

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

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
2	1	mopntopon	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{TopOn}\left(X\right)$$
3		toponss	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge A\in J\right)\to A\subseteq X$$
4	2 3	sylan	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in J\right)\to A\subseteq X$$