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	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	mopnfss	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ⊆ 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		pwuni	⊢ 𝐽 ⊆ 𝒫 ∪ 𝐽
3	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4	3	pweqd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝒫 𝑋 = 𝒫 ∪ 𝐽 )
5	2 4	sseqtrrid	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ⊆ 𝒫 𝑋 )