![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > blssm | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
blssm | ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋) |
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‘𝐷)𝑅) ⊆ 𝑋) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |