This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Open sets of a metric space mopnm
Description: The base set of a metric space is open. Part of Theorem T1 of
Kreyszig p. 19. (Contributed by NM , 4-Sep-2006) (Revised by Mario
Carneiro , 12-Nov-2013)
Ref
Expression
Hypothesis
mopnval.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion
mopnm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
Proof
Step
Hyp
Ref
Expression
1
mopnval.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2
1
mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3
toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
4
2 3
syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )