MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blssm Unicode version

Theorem blssm 18343
Description: A ball is a subset of the base set of a metric space. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
Assertion
Ref Expression
blssm  |-  ( ( D  e.  ( * Met `  X )  /\  P  e.  X  /\  R  e.  RR* )  ->  ( P ( ball `  D ) R ) 
C_  X )

Proof of Theorem blssm
StepHypRef Expression
1 blf 18336 . . 3  |-  ( D  e.  ( * Met `  X )  ->  ( ball `  D ) : ( X  X.  RR* )
--> ~P X )
2 fovrn 6156 . . 3  |-  ( ( ( ball `  D
) : ( X  X.  RR* ) --> ~P X  /\  P  e.  X  /\  R  e.  RR* )  ->  ( P ( ball `  D ) R )  e.  ~P X )
31, 2syl3an1 1217 . 2  |-  ( ( D  e.  ( * Met `  X )  /\  P  e.  X  /\  R  e.  RR* )  ->  ( P ( ball `  D ) R )  e.  ~P X )
43elpwid 3752 1  |-  ( ( D  e.  ( * Met `  X )  /\  P  e.  X  /\  R  e.  RR* )  ->  ( P ( ball `  D ) R ) 
C_  X )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    e. wcel 1717    C_ wss 3264   ~Pcpw 3743    X. cxp 4817   -->wf 5391   ` cfv 5395  (class class class)co 6021   RR*cxr 9053   * Metcxmt 16613   ballcbl 16615
This theorem is referenced by:  blpnfctr  18357  xmetresbl  18358  imasf1oxms  18410  prdsbl  18412  blcld  18426  blcls  18427  prdsxmslem2  18450  metcnp  18462  cnllycmp  18853  lebnumlem3  18860  lebnum  18861  cfil3i  19094  iscfil3  19098  cfilfcls  19099  iscmet3lem2  19117  equivcfil  19124  caublcls  19133  relcmpcmet  19141  cmpcmet  19142  cncmet  19145  bcthlem2  19148  bcthlem4  19150  dvlip2  19747  dv11cn  19753  pserdvlem2  20212  pserdv  20213  abelthlem3  20217  abelthlem5  20219  dvlog2lem  20411  dvlog2  20412  efopnlem2  20416  efopn  20417  logtayl  20419  efrlim  20676  blscon  24711  sstotbnd2  26175  equivtotbnd  26179  isbnd2  26184  blbnd  26188  totbndbnd  26190  prdstotbnd  26195  prdsbnd2  26196  ismtyima  26204  heiborlem3  26214  heiborlem8  26219
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-cnex 8980  ax-resscn 8981
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-fv 5403  df-ov 6024  df-oprab 6025  df-mpt2 6026  df-1st 6289  df-2nd 6290  df-map 6957  df-xr 9058  df-xmet 16620  df-bl 16622
  Copyright terms: Public domain W3C validator