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 = ( w e. _V |-> ( x e. ( Base ` w ) , r e. ( 0 [,] +oo ) |-> { p e. ( Base ` w ) | ( p ( dist ` w ) x ) = r } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csph	|- Sphere
1		vw	|- w
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7		vr	|- r
8		cc0	|- 0
9		cicc	|- [,]
10		cpnf	|- +oo
11	8 10 9	co	|- ( 0 [,] +oo )
12		vp	|- p
13	12	cv	|- p
14		cds	|- dist
15	5 14	cfv	|- ( dist ` w )
16	3	cv	|- x
17	13 16 15	co	|- ( p ( dist ` w ) x )
18	7	cv	|- r
19	17 18	wceq	|- ( p ( dist ` w ) x ) = r
20	19 12 6	crab	|- { p e. ( Base ` w ) | ( p ( dist ` w ) x ) = r }
21	3 7 6 11 20	cmpo	|- ( x e. ( Base ` w ) , r e. ( 0 [,] +oo ) |-> { p e. ( Base ` w ) | ( p ( dist ` w ) x ) = r } )
22	1 2 21	cmpt	|- ( w e. _V |-> ( x e. ( Base ` w ) , r e. ( 0 [,] +oo ) |-> { p e. ( Base ` w ) | ( p ( dist ` w ) x ) = r } ) )
23	0 22	wceq	|- Sphere = ( w e. _V |-> ( x e. ( Base ` w ) , r e. ( 0 [,] +oo ) |-> { p e. ( Base ` w ) | ( p ( dist ` w ) x ) = r } ) )