Metamath Proof Explorer

Theorem mopni2

Description: An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopni.1 
|- J = ( MetOpen ` D )
Assertion mopni2 
|- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ A )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 1 mopni 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. y e. ran ( ball ` D ) ( P e. y /\ y C_ A ) )
3 1 mopnss 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J ) -> A C_ X )
4 3 sselda 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J ) /\ P e. A ) -> P e. X )
5 blssex 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. y e. ran ( ball ` D ) ( P e. y /\ y C_ A ) <-> E. x e. RR+ ( P ( ball ` D ) x ) C_ A ) )
6 5 adantlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J ) /\ P e. X ) -> ( E. y e. ran ( ball ` D ) ( P e. y /\ y C_ A ) <-> E. x e. RR+ ( P ( ball ` D ) x ) C_ A ) )
7 4 6 syldan 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. J ) /\ P e. A ) -> ( E. y e. ran ( ball ` D ) ( P e. y /\ y C_ A ) <-> E. x e. RR+ ( P ( ball ` D ) x ) C_ A ) )
8 7 3impa 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> ( E. y e. ran ( ball ` D ) ( P e. y /\ y C_ A ) <-> E. x e. RR+ ( P ( ball ` D ) x ) C_ A ) )
9 2 8 mpbid 
 |-  ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ A )