| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > blcntr | Structured version Visualization version GIF version | ||
| Description: A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| Ref | Expression |
|---|---|
| blcntr | ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rpxr 13010 | . . 3 ⊢ (𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ*) | |
| 2 | rpgt0 13013 | . . 3 ⊢ (𝑅 ∈ ℝ+ → 0 < 𝑅) | |
| 3 | 1, 2 | jca 511 | . 2 ⊢ (𝑅 ∈ ℝ+ → (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) |
| 4 | xblcntr 24335 | . 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | |
| 5 | 3, 4 | syl3an3 1165 | 1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2107 class class class wbr 5116 ‘cfv 6527 (class class class)co 7399 0cc0 11121 ℝ*cxr 11260 < clt 11261 ℝ+crp 13000 ∞Metcxmet 21285 ballcbl 21287 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-sep 5263 ax-nul 5273 ax-pow 5332 ax-pr 5399 ax-un 7723 ax-cnex 11177 ax-resscn 11178 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-rab 3414 df-v 3459 df-sbc 3764 df-csb 3873 df-dif 3927 df-un 3929 df-in 3931 df-ss 3941 df-nul 4307 df-if 4499 df-pw 4575 df-sn 4600 df-pr 4602 df-op 4606 df-uni 4881 df-iun 4966 df-br 5117 df-opab 5179 df-mpt 5199 df-id 5545 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6480 df-fun 6529 df-fn 6530 df-f 6531 df-fv 6535 df-ov 7402 df-oprab 7403 df-mpo 7404 df-1st 7982 df-2nd 7983 df-map 8836 df-xr 11265 df-rp 13001 df-psmet 21292 df-xmet 21293 df-bl 21295 |
| This theorem is referenced by: bln0 24339 unirnbl 24344 blssex 24351 neibl 24425 blnei 24426 metss 24432 methaus 24444 met1stc 24445 met2ndci 24446 metrest 24448 prdsxmslem2 24453 metcnp3 24464 tgioo 24720 zdis 24741 metnrmlem2 24785 cnllycmp 24891 nmhmcn 25056 lmmbr 25195 cfilfcls 25211 iscmet3lem2 25229 caubl 25245 caublcls 25246 flimcfil 25251 ellimc3 25817 ulmdvlem1 26346 efopn 26603 logtayl 26605 xrlimcnp 26914 efrlim 26915 efrlimOLD 26916 lgamucov 26984 cnllysconn 35188 poimirlem30 37595 blbnd 37732 heibor1lem 37754 heibor1 37755 binomcxplemnotnn0 44306 hoiqssbl 46584 |
| Copyright terms: Public domain | W3C validator |