Theorem mopnfss

Description: The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
2		pwuni	$$⊢J\subseteq 𝒫\bigcup J$$
3	1	mopnuni	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X=\bigcup J$$
4	3	pweqd	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to 𝒫X=𝒫\bigcup J$$
5	2 4	sseqtrrid	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\subseteq 𝒫X$$