Metamath Proof Explorer

Theorem blnei

Description: A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis mopni.1 
|- J = ( MetOpen ` D )
Assertion blnei 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
3 2 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> J e. Top )
4 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
5 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. J )
6 4 5 syl3an3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. J )
7 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> P e. ( P ( ball ` D ) R ) )
8 opnneip 
 |-  ( ( J e. Top /\ ( P ( ball ` D ) R ) e. J /\ P e. ( P ( ball ` D ) R ) ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )
9 3 6 7 8 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )