Definition df-sph

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

	Ref	Expression
Assertion	df-sph	$$⊢Sphere=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w,r\in \left[0,\mathrm{+\infty }\right]⟼\left\{p\in {\mathrm{Base}}_w|p\mathrm{dist}\left(w\right)x=r\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csph	$$classSphere$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7		vr	$$setvarr$$
8		cc0	$$class0$$
9		cicc	$$class\left[.\right]$$
10		cpnf	$$class\mathrm{+\infty }$$
11	8 10 9	co	$$class\left[0,\mathrm{+\infty }\right]$$
12		vp	$$setvarp$$
13	12	cv	$$setvarp$$
14		cds	$$class\mathrm{dist}$$
15	5 14	cfv	$$class\mathrm{dist}\left(w\right)$$
16	3	cv	$$setvarx$$
17	13 16 15	co	$$class\left(p\mathrm{dist}\left(w\right)x\right)$$
18	7	cv	$$setvarr$$
19	17 18	wceq	$$wffp\mathrm{dist}\left(w\right)x=r$$
20	19 12 6	crab	$$class\left\{p\in {\mathrm{Base}}_w|p\mathrm{dist}\left(w\right)x=r\right\}$$
21	3 7 6 11 20	cmpo	$$class\left(x\in {\mathrm{Base}}_w,r\in \left[0,\mathrm{+\infty }\right]⟼\left\{p\in {\mathrm{Base}}_w|p\mathrm{dist}\left(w\right)x=r\right\}\right)$$
22	1 2 21	cmpt	$$class\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w,r\in \left[0,\mathrm{+\infty }\right]⟼\left\{p\in {\mathrm{Base}}_w|p\mathrm{dist}\left(w\right)x=r\right\}\right)\right)$$
23	0 22	wceq	$$wffSphere=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w,r\in \left[0,\mathrm{+\infty }\right]⟼\left\{p\in {\mathrm{Base}}_w|p\mathrm{dist}\left(w\right)x=r\right\}\right)\right)$$