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

Metamath Proof Explorer

Theorem mopnval

Description: An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of Kreyszig p. 18. The object ( MetOpenD ) is the family of all open sets in the metric space determined by the metric D . By mopntop , the open sets of a metric space form a topology J , whose base set is U. J by mopnuni . (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 fvssunirn ⊢ ( ∞Met ‘ 𝑋 ) ⊆ ∪ ran ∞Met
3 2 sseli ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ∪ ran ∞Met )
4 fveq2 ⊢ ( 𝑑 = 𝐷 → ( ball ‘ 𝑑 ) = ( ball ‘ 𝐷 ) )
5 4 rneqd ⊢ ( 𝑑 = 𝐷 → ran ( ball ‘ 𝑑 ) = ran ( ball ‘ 𝐷 ) )
6 5 fveq2d ⊢ ( 𝑑 = 𝐷 → ( topGen ‘ ran ( ball ‘ 𝑑 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
7 df-mopn ⊢ MetOpen = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )
8 fvex ⊢ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ∈ V
9 6 7 8 fvmpt ⊢ ( 𝐷 ∈ ∪ ran ∞Met → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
10 1 9 eqtrid ⊢ ( 𝐷 ∈ ∪ ran ∞Met → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
11 3 10 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )