Metamath Proof Explorer

Theorem mopntop

Description: The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopnval.1 
|- J = ( MetOpen ` D )
Assertion mopntop 
|- ( D e. ( *Met ` X ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 mopnval.1 
 |-  J = ( MetOpen ` D )
2 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
3 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
4 2 3 syl 
 |-  ( D e. ( *Met ` X ) -> J e. Top )