Theorem blssm 22725

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 22714	. . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋)
2		fovrn 7132	. . 3 ⊢ (((ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋 ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝒫 𝑋)
3	1, 2	syl3an1 1143	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝒫 𝑋)
4	3	elpwid 4432	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋)

Syntax hints:   → wi 4   ∧ w3a 1068   ∈ wcel 2048   ⊆ wss 3828  𝒫 cpw 4420   × cxp 5402  ⟶wf 6182  ‘cfv 6186  (class class class)co 6974  ℝ^*cxr 10469  ∞Metcxmet 20226  ballcbl 20228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-cnex 10387  ax-resscn 10388

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-fv 6194  df-ov 6977  df-oprab 6978  df-mpo 6979  df-1st 7498  df-2nd 7499  df-map 8204  df-xr 10474  df-psmet 20233  df-xmet 20234  df-bl 20236

This theorem is referenced by:  blpnfctr  22743  xmetresbl  22744  imasf1oxms  22796  prdsbl  22798  blcld  22812  blcls  22813  prdsxmslem2  22836  metcnp  22848  cnllycmp  23257  lebnumlem3  23264  lebnum  23265  cfil3i  23569  iscfil3  23573  cfilfcls  23574  iscmet3lem2  23592  equivcfil  23599  caublcls  23609  relcmpcmet  23618  cmpcmet  23619  cncmet  23622  bcthlem2  23625  bcthlem4  23627  dvlip2  24289  dv11cn  24295  pserdvlem2  24713  pserdv  24714  abelthlem3  24718  abelthlem5  24720  dvlog2lem  24930  dvlog2  24931  efopnlem2  24935  efopn  24936  logtayl  24938  efrlim  25243  blsconn  32066  sstotbnd2  34472  equivtotbnd  34476  isbnd2  34481  blbnd  34485  totbndbnd  34487  prdstotbnd  34492  prdsbnd2  34493  ismtyima  34501  heiborlem3  34511  heiborlem8  34516