Theorem blssm 24465

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	⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋)

Proof of Theorem blssm

Step	Hyp	Ref	Expression
1		blf 24454	. . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋)
2		fovcdm 7560	. . 3 ⊢ (((ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋 ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝒫 𝑋)
3	1, 2	syl3an1 1175	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝒫 𝑋)
4	3	elpwid 4561	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ w3a 1097   ∈ wcel 2141   ⊆ wss 3902  𝒫 cpw 4552   × cxp 5641  ⟶wf 6511  ‘cfv 6515  (class class class)co 7390  ℝ^*cxr 11208  ∞Metcxmet 21396  ballcbl 21398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7964  df-2nd 7965  df-map 8803  df-xr 11213  df-psmet 21403  df-xmet 21404  df-bl 21406

This theorem is referenced by:  blpnfctr  24483  xmetresbl  24484  imasf1oxms  24536  prdsbl  24538  blcld  24552  blcls  24553  prdsxmslem2  24576  metcnp  24588  cnllycmp  25005  lebnumlem3  25012  lebnum  25013  cfil3i  25318  iscfil3  25322  cfilfcls  25323  iscmet3lem2  25341  equivcfil  25348  caublcls  25358  relcmpcmet  25367  cmpcmet  25368  cncmet  25371  bcthlem2  25374  bcthlem4  25376  dvlip2  26044  dv11cn  26050  pserdvlem2  26478  pserdv  26479  abelthlem3  26483  abelthlem5  26485  dvlog2lem  26704  dvlog2  26705  efopnlem2  26709  efopn  26710  logtayl  26712  efrlim  27021  blsconn  35554  sstotbnd2  38233  equivtotbnd  38237  isbnd2  38242  blbnd  38246  totbndbnd  38248  prdstotbnd  38253  prdsbnd2  38254  ismtyima  38262  heiborlem3  38272  heiborlem8  38277