Theorem spheres

Description: The spheres for given centers and radii in a metric space (or any extensible structure having a base set and a distance function). (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	spheres.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	spheres.l	⊢ 𝑆 = ( Sphere ‘ 𝑊 )
	spheres.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
Assertion	spheres	⊢ ( 𝑊 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )

Proof

Step	Hyp	Ref	Expression
1		spheres.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		spheres.l	⊢ 𝑆 = ( Sphere ‘ 𝑊 )
3		spheres.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
4	2	a1i	⊢ ( 𝑊 ∈ 𝑉 → 𝑆 = ( Sphere ‘ 𝑊 ) )
5		df-sph	⊢ Sphere = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } ) )
6		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
7	1	eqcomi	⊢ ( Base ‘ 𝑊 ) = 𝐵
8	7	a1i	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑊 ) = 𝐵 )
9	6 8	eqtrd	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
10		eqidd	⊢ ( 𝑤 = 𝑊 → ( 0 [,] +∞ ) = ( 0 [,] +∞ ) )
11		fveq2	⊢ ( 𝑤 = 𝑊 → ( dist ‘ 𝑤 ) = ( dist ‘ 𝑊 ) )
12	3	eqcomi	⊢ ( dist ‘ 𝑊 ) = 𝐷
13	12	a1i	⊢ ( 𝑤 = 𝑊 → ( dist ‘ 𝑊 ) = 𝐷 )
14	11 13	eqtrd	⊢ ( 𝑤 = 𝑊 → ( dist ‘ 𝑤 ) = 𝐷 )
15	14	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = ( 𝑝 𝐷 𝑥 ) )
16	15	eqeq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 ↔ ( 𝑝 𝐷 𝑥 ) = 𝑟 ) )
17	9 16	rabeqbidv	⊢ ( 𝑤 = 𝑊 → { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } = { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } )
18	9 10 17	mpoeq123dv	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑝 ( dist ‘ 𝑤 ) 𝑥 ) = 𝑟 } ) = ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )
19		elex	⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
20		fvex	⊢ ( Base ‘ 𝑊 ) ∈ V
21	1 20	eqeltri	⊢ 𝐵 ∈ V
22		ovex	⊢ ( 0 [,] +∞ ) ∈ V
23	21 22	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) ∈ V
24	23	a1i	⊢ ( 𝑊 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) ∈ V )
25	5 18 19 24	fvmptd3	⊢ ( 𝑊 ∈ 𝑉 → ( Sphere ‘ 𝑊 ) = ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )
26	4 25	eqtrd	⊢ ( 𝑊 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )