Metamath Proof Explorer

Theorem rnblopn

Description: A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006)

Ref Expression
Hypothesis mopni.1 
|- J = ( MetOpen ` D )
Assertion rnblopn 
|- ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) ) -> B e. J )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 1 blssopn 
 |-  ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J )
3 2 sselda 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) ) -> B e. J )