Metamath Proof Explorer

Theorem blssec

Description: A ball centered at P is contained in the set of points finitely separated from P . This is just an application of ssbl to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis xmeter.1 
|- .~ = ( `' D " RR )
Assertion blssec 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` D ) S ) C_ [ P ] .~ )

Proof

Step Hyp Ref Expression
1 xmeter.1 
 |-  .~ = ( `' D " RR )
2 pnfge 
 |-  ( S e. RR* -> S <_ +oo )
3 2 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ S e. RR* ) -> S <_ +oo )
4 pnfxr 
 |-  +oo e. RR*
5 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( S e. RR* /\ +oo e. RR* ) /\ S <_ +oo ) -> ( P ( ball ` D ) S ) C_ ( P ( ball ` D ) +oo ) )
6 5 3expia 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( S e. RR* /\ +oo e. RR* ) ) -> ( S <_ +oo -> ( P ( ball ` D ) S ) C_ ( P ( ball ` D ) +oo ) ) )
7 4 6 mpanr2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ S e. RR* ) -> ( S <_ +oo -> ( P ( ball ` D ) S ) C_ ( P ( ball ` D ) +oo ) ) )
8 3 7 mpd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ S e. RR* ) -> ( P ( ball ` D ) S ) C_ ( P ( ball ` D ) +oo ) )
9 8 3impa 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` D ) S ) C_ ( P ( ball ` D ) +oo ) )
10 1 xmetec 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> [ P ] .~ = ( P ( ball ` D ) +oo ) )
11 10 3adant3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> [ P ] .~ = ( P ( ball ` D ) +oo ) )
12 9 11 sseqtrrd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` D ) S ) C_ [ P ] .~ )