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 ) )