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 ⊢ J = MetOpen ⁡ D
Assertion mopntopon ⊢ D ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢ J = MetOpen ⁡ D
2 1 mopnval ⊢ D ∈ ∞Met ⁡ X → J = topGen ⁡ ran ⁡ ball ⁡ D
3 blbas ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ∈ TopBases
4 tgtopon ⊢ ran ⁡ ball ⁡ D ∈ TopBases → topGen ⁡ ran ⁡ ball ⁡ D ∈ TopOn ⁡ ⋃ ran ⁡ ball ⁡ D
5 3 4 syl ⊢ D ∈ ∞Met ⁡ X → topGen ⁡ ran ⁡ ball ⁡ D ∈ TopOn ⁡ ⋃ ran ⁡ ball ⁡ D
6 unirnbl ⊢ D ∈ ∞Met ⁡ X → ⋃ ran ⁡ ball ⁡ D = X
7 6 fveq2d ⊢ D ∈ ∞Met ⁡ X → TopOn ⁡ ⋃ ran ⁡ ball ⁡ D = TopOn ⁡ X
8 5 7 eleqtrd ⊢ D ∈ ∞Met ⁡ X → topGen ⁡ ran ⁡ ball ⁡ D ∈ TopOn ⁡ X
9 2 8 eqeltrd ⊢ D ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X