Definition df-sph 47464

Description: Definition of spheres for given centers and radii in a metric space (or more generally, in a distance space, see distspace 23822, or even in any extended structure having a base set and a distance function into the real numbers. (Contributed by AV, 14-Jan-2023.)

Assertion

Ref	Expression
df-sph	⊢ Sphere = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))

Distinct variable group:   𝑟,𝑝,𝑤,𝑥

Detailed syntax breakdown of Definition df-sph

Step	Hyp	Ref	Expression
1		csph 47462	. 2 class Sphere
2		vw	. . 3 setvar 𝑤
3		cvv 3475	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vr	. . . 4 setvar 𝑟
6	2	cv 1541	. . . . 5 class 𝑤
7		cbs 17144	. . . . 5 class Base
8	6, 7	cfv 6544	. . . 4 class (Base‘𝑤)
9		cc0 11110	. . . . 5 class 0
10		cpnf 11245	. . . . 5 class +∞
11		cicc 13327	. . . . 5 class [,]
12	9, 10, 11	co 7409	. . . 4 class (0[,]+∞)
13		vp	. . . . . . . 8 setvar 𝑝
14	13	cv 1541	. . . . . . 7 class 𝑝
15	4	cv 1541	. . . . . . 7 class 𝑥
16		cds 17206	. . . . . . . 8 class dist
17	6, 16	cfv 6544	. . . . . . 7 class (dist‘𝑤)
18	14, 15, 17	co 7409	. . . . . 6 class (𝑝(dist‘𝑤)𝑥)
19	5	cv 1541	. . . . . 6 class 𝑟
20	18, 19	wceq 1542	. . . . 5 wff (𝑝(dist‘𝑤)𝑥) = 𝑟
21	20, 13, 8	crab 3433	. . . 4 class {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}
22	4, 5, 8, 12, 21	cmpo 7411	. . 3 class (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟})
23	2, 3, 22	cmpt 5232	. 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))
24	1, 23	wceq 1542	1 wff Sphere = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑟 ∈ (0[,]+∞) ↦ {𝑝 ∈ (Base‘𝑤) ∣ (𝑝(dist‘𝑤)𝑥) = 𝑟}))

This definition is referenced by:  spheres  47480