Metamath Proof Explorer

Theorem mopnss

Description: An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006)

Ref Expression
Hypothesis mopnval.1 
|- J = ( MetOpen ` D )
Assertion mopnss 
|- ( ( D e. ( *Met ` X ) /\ A e. J ) -> A C_ X )

Proof

Step Hyp Ref Expression
1 mopnval.1 
 |-  J = ( MetOpen ` D )
2 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
3 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. J ) -> A C_ X )
4 2 3 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J ) -> A C_ X )