| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > blelrn | GIF version | ||
| Description: A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| Ref | Expression |
|---|---|
| blelrn | ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | blf 15043 | . . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋) | |
| 2 | 1 | ffnd 5447 | . 2 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) Fn (𝑋 × ℝ*)) |
| 3 | fnovrn 6119 | . 2 ⊢ (((ball‘𝐷) Fn (𝑋 × ℝ*) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) | |
| 4 | 2, 3 | syl3an1 1283 | 1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ w3a 981 ∈ wcel 2178 𝒫 cpw 3627 × cxp 4692 ran crn 4695 Fn wfn 5286 ‘cfv 5291 (class class class)co 5969 ℝ*cxr 8143 ∞Metcxmet 14459 ballcbl 14461 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-sep 4179 ax-pow 4235 ax-pr 4270 ax-un 4499 ax-setind 4604 ax-cnex 8053 ax-resscn 8054 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-ral 2491 df-rex 2492 df-rab 2495 df-v 2779 df-sbc 3007 df-csb 3103 df-dif 3177 df-un 3179 df-in 3181 df-ss 3188 df-pw 3629 df-sn 3650 df-pr 3651 df-op 3653 df-uni 3866 df-iun 3944 df-br 4061 df-opab 4123 df-mpt 4124 df-id 4359 df-xp 4700 df-rel 4701 df-cnv 4702 df-co 4703 df-dm 4704 df-rn 4705 df-res 4706 df-ima 4707 df-iota 5252 df-fun 5293 df-fn 5294 df-f 5295 df-fv 5299 df-ov 5972 df-oprab 5973 df-mpo 5974 df-1st 6251 df-2nd 6252 df-map 6762 df-pnf 8146 df-mnf 8147 df-xr 8148 df-psmet 14466 df-xmet 14467 df-bl 14469 |
| This theorem is referenced by: unirnbl 15056 blssex 15063 blopn 15123 metss 15127 metcnp3 15144 ioo2blex 15185 |
| Copyright terms: Public domain | W3C validator |