Metamath Proof Explorer

Theorem blcls

Description: The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses mopni.1 
|- J = ( MetOpen ` D )
blcld.3 
|- S = { z e. X | ( P D z ) <_ R }
Assertion blcls 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ S )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 blcld.3 
 |-  S = { z e. X | ( P D z ) <_ R }
3 1 2 blcld 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> S e. ( Clsd ` J ) )
4 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ X )
5 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( z e. ( P ( ball ` D ) R ) <-> ( z e. X /\ ( P D z ) < R ) ) )
6 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ z e. X ) -> ( P D z ) e. RR* )
7 6 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ z e. X ) -> ( P D z ) e. RR* )
8 7 3adantl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ z e. X ) -> ( P D z ) e. RR* )
9 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ z e. X ) -> R e. RR* )
10 xrltle 
 |-  ( ( ( P D z ) e. RR* /\ R e. RR* ) -> ( ( P D z ) < R -> ( P D z ) <_ R ) )
11 8 9 10 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ z e. X ) -> ( ( P D z ) < R -> ( P D z ) <_ R ) )
12 11 expimpd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( z e. X /\ ( P D z ) < R ) -> ( P D z ) <_ R ) )
13 5 12 sylbid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( z e. ( P ( ball ` D ) R ) -> ( P D z ) <_ R ) )
14 13 ralrimiv 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> A. z e. ( P ( ball ` D ) R ) ( P D z ) <_ R )
15 ssrab 
 |-  ( ( P ( ball ` D ) R ) C_ { z e. X | ( P D z ) <_ R } <-> ( ( P ( ball ` D ) R ) C_ X /\ A. z e. ( P ( ball ` D ) R ) ( P D z ) <_ R ) )
16 4 14 15 sylanbrc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ { z e. X | ( P D z ) <_ R } )
17 16 2 sseqtrrdi 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ S )
18 eqid 
 |-  U. J = U. J
19 18 clsss2 
 |-  ( ( S e. ( Clsd ` J ) /\ ( P ( ball ` D ) R ) C_ S ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ S )
20 3 17 19 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ S )