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 = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csph	⊢ Sphere
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7		vr	⊢ 𝑟
8		cc0	⊢ 0
9		cicc	⊢ [,]
10		cpnf	⊢ +∞
11	8 10 9	co	⊢ ( 0 [,] +∞ )
12		vp	⊢ 𝑝
13	12	cv	⊢ 𝑝
14		cds	⊢ dist
15	5 14	cfv	⊢ ( dist ‘ 𝑤 )
16	3	cv	⊢ 𝑥
17	13 16 15	co	⊢ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 )
18	7	cv	⊢ 𝑟
19	17 18	wceq	⊢ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟
20	19 12 6	crab	⊢ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 }
21	3 7 6 11 20	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } )
22	1 2 21	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } ) )
23	0 22	wceq	⊢ Sphere = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } ) )