![]() |
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 12248 | . . 3 ⊢ (𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ*) | |
2 | rpgt0 12251 | . . 3 ⊢ (𝑅 ∈ ℝ+ → 0 < 𝑅) | |
3 | 1, 2 | jca 512 | . 2 ⊢ (𝑅 ∈ ℝ+ → (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) |
4 | xblcntr 22704 | . 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | |
5 | 3, 4 | syl3an3 1158 | 1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 ∈ wcel 2081 class class class wbr 4962 ‘cfv 6225 (class class class)co 7016 0cc0 10383 ℝ*cxr 10520 < clt 10521 ℝ+crp 12239 ∞Metcxmet 20212 ballcbl 20214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-1st 7545 df-2nd 7546 df-map 8258 df-xr 10525 df-rp 12240 df-psmet 20219 df-xmet 20220 df-bl 20222 |
This theorem is referenced by: bln0 22708 unirnbl 22713 blssex 22720 neibl 22794 blnei 22795 metss 22801 methaus 22813 met1stc 22814 met2ndci 22815 metrest 22817 prdsxmslem2 22822 metcnp3 22833 tgioo 23087 zdis 23107 metnrmlem2 23151 cnllycmp 23243 nmhmcn 23407 lmmbr 23544 cfilfcls 23560 iscmet3lem2 23578 caubl 23594 caublcls 23595 flimcfil 23600 ellimc3 24160 ulmdvlem1 24671 efopn 24922 logtayl 24924 xrlimcnp 25228 efrlim 25229 lgamucov 25297 cnllysconn 32100 poimirlem30 34453 blbnd 34597 heibor1lem 34619 heibor1 34620 binomcxplemnotnn0 40226 hoiqssbl 42449 |
Copyright terms: Public domain | W3C validator |