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 
|- J = ( MetOpen ` D )
Assertion mopnval 
|- ( D e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` D ) ) )

Proof

Step Hyp Ref Expression
1 mopnval.1 
 |-  J = ( MetOpen ` D )
2 fvssunirn 
 |-  ( *Met ` X ) C_ U. ran *Met
3 2 sseli 
 |-  ( D e. ( *Met ` X ) -> D e. U. ran *Met )
4 fveq2 
 |-  ( d = D -> ( ball ` d ) = ( ball ` D ) )
5 4 rneqd 
 |-  ( d = D -> ran ( ball ` d ) = ran ( ball ` D ) )
6 5 fveq2d 
 |-  ( d = D -> ( topGen ` ran ( ball ` d ) ) = ( topGen ` ran ( ball ` D ) ) )
7 df-mopn 
 |-  MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
8 fvex 
 |-  ( topGen ` ran ( ball ` D ) ) e. _V
9 6 7 8 fvmpt 
 |-  ( D e. U. ran *Met -> ( MetOpen ` D ) = ( topGen ` ran ( ball ` D ) ) )
10 1 9 eqtrid 
 |-  ( D e. U. ran *Met -> J = ( topGen ` ran ( ball ` D ) ) )
11 3 10 syl 
 |-  ( D e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` D ) ) )