blelrn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > blelrn		Structured version Visualization version GIF version

Theorem blelrn 22444

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.)

**Assertion**
Ref	Expression
blelrn	⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷))

**Proof of Theorem blelrn**
Step	Hyp	Ref	Expression
1		blf 22434	. . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ^*)⟶𝒫 𝑋)
2		ffn 6207	. . 3 ⊢ ((ball‘𝐷):(𝑋 × ℝ^)⟶𝒫 𝑋 → (ball‘𝐷) Fn (𝑋 × ℝ^))
3	1, 2	syl 17	. 2 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) Fn (𝑋 × ℝ^*))
4		fnovrn 6976	. 2 ⊢ (((ball‘𝐷) Fn (𝑋 × ℝ^) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷))
5	3, 4	syl3an1 1167	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1072 ∈ wcel 2140 𝒫 cpw 4303 × cxp 5265 ran crn 5268 Fn wfn 6045 ⟶wf 6046 ‘cfv 6050 (class class class)co 6815 ℝ^*cxr 10286 ∞Metcxmt 19954 ballcbl 19956

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 ax-cnex 10205 ax-resscn 10206

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-op 4329 df-uni 4590 df-iun 4675 df-br 4806 df-opab 4866 df-mpt 4883 df-id 5175 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-fv 6058 df-ov 6818 df-oprab 6819 df-mpt2 6820 df-1st 7335 df-2nd 7336 df-map 8028 df-xr 10291 df-psmet 19961 df-xmet 19962 df-bl 19964

This theorem is referenced by: unirnbl 22447 blssex 22454 blopn 22527 blcld 22532 metss 22535 metcnp3 22567 dscopn 22600 ioo2blex 22819

W3C validator