Theorem blssm 24556

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 24545	. . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋)
2		fovcdm 7582	. . 3 ⊢ (((ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋 ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝒫 𝑋)
3	1, 2	syl3an1 1181	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝒫 𝑋)
4	3	elpwid 4572	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ w3a 1103   ∈ wcel 2143   ⊆ wss 3906  𝒫 cpw 4563   × cxp 5661  ⟶wf 6534  ‘cfv 6538  (class class class)co 7412  ℝ^*cxr 11243  ∞Metcxmet 21488  ballcbl 21490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7987  df-2nd 7988  df-map 8827  df-xr 11248  df-psmet 21495  df-xmet 21496  df-bl 21498

This theorem is referenced by:  blpnfctr  24574  xmetresbl  24575  imasf1oxms  24627  prdsbl  24629  blcld  24643  blcls  24644  prdsxmslem2  24667  metcnp  24679  cnllycmp  25096  lebnumlem3  25103  lebnum  25104  cfil3i  25409  iscfil3  25413  cfilfcls  25414  iscmet3lem2  25432  equivcfil  25439  caublcls  25449  relcmpcmet  25458  cmpcmet  25459  cncmet  25462  bcthlem2  25465  bcthlem4  25467  dvlip2  26135  dv11cn  26141  pserdvlem2  26572  pserdv  26573  abelthlem3  26577  abelthlem5  26579  dvlog2lem  26798  dvlog2  26799  efopnlem2  26803  efopn  26804  logtayl  26806  efrlim  27115  blsconn  35717  sstotbnd2  38406  equivtotbnd  38410  isbnd2  38415  blbnd  38419  totbndbnd  38421  prdstotbnd  38426  prdsbnd2  38427  ismtyima  38435  heiborlem3  38445  heiborlem8  38450