This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blsscls

Description: If two concentric balls have different radii, the closure of the smaller one is contained in the larger one. (Contributed by Mario Carneiro, 5-Jan-2014)

Ref Expression
Hypothesis blsscls.2 
|- J = ( MetOpen ` D )
Assertion blsscls 
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* /\ R < S ) ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ ( P ( ball ` D ) S ) )

Proof

Step Hyp Ref Expression
1 blsscls.2 
 |-  J = ( MetOpen ` D )
2 eqid 
 |-  { x e. X | ( P D x ) <_ R } = { x e. X | ( P D x ) <_ R }
3 1 2 blcls 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ { x e. X | ( P D x ) <_ R } )
4 3 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ R e. RR* ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ { x e. X | ( P D x ) <_ R } )
5 4 3ad2antr1 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* /\ R < S ) ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ { x e. X | ( P D x ) <_ R } )
6 1 2 blsscls2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* /\ R < S ) ) -> { x e. X | ( P D x ) <_ R } C_ ( P ( ball ` D ) S ) )
7 5 6 sstrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* /\ R < S ) ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ ( P ( ball ` D ) S ) )