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 β€˜ 𝐷 ) ) )