Metamath Proof Explorer

Theorem xmetutop

Description: The topology induced by a uniform structure generated by an extended metric D is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion xmetutop 
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( MetOpen ` D ) )

Proof

Step Hyp Ref Expression
1 xmetpsmet 
 |-  ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )
2 psmetutop 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( topGen ` ran ( ball ` D ) ) )
3 1 2 sylan2 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( topGen ` ran ( ball ` D ) ) )
4 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
5 4 mopnval 
 |-  ( D e. ( *Met ` X ) -> ( MetOpen ` D ) = ( topGen ` ran ( ball ` D ) ) )
6 5 adantl 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( MetOpen ` D ) = ( topGen ` ran ( ball ` D ) ) )
7 3 6 eqtr4d 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( MetOpen ` D ) )