This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mopntopon

Description: The set of open sets of a metric space X is a topology on X . Remark in Kreyszig p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis mopnval.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion mopntopon ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopnval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
3 blbas ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ∈ TopBases )
4 tgtopon ⊢ ( ran ( ball ‘ 𝐷 ) ∈ TopBases → ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ∈ ( TopOn ‘ ∪ ran ( ball ‘ 𝐷 ) ) )
5 3 4 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ∈ ( TopOn ‘ ∪ ran ( ball ‘ 𝐷 ) ) )
6 unirnbl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
7 6 fveq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( TopOn ‘ ∪ ran ( ball ‘ 𝐷 ) ) = ( TopOn ‘ 𝑋 ) )
8 5 7 eleqtrd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ∈ ( TopOn ‘ 𝑋 ) )
9 2 8 eqeltrd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )