Theorem mopn0

Description: The empty set is an open set of a metric space. Part of Theorem T1 of Kreyszig p. 19. (Contributed by NM, 4-Sep-2006)

	Ref	Expression
Hypothesis	mopni.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	mopn0	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∅ ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		mopni.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3		0opn	⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
4	2 3	syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∅ ∈ 𝐽 )