Theorem sphere

Description: A sphere with center X and radius R 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	sphere	⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → ( 𝑋 𝑆 𝑅 ) = { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑋 ) = 𝑅 } )

Proof

Step	Hyp	Ref	Expression
1		spheres.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		spheres.l	⊢ 𝑆 = ( Sphere ‘ 𝑊 )
3		spheres.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
4	1 2 3	spheres	⊢ ( 𝑊 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )
5	4	3ad2ant1	⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑟 ∈ ( 0 [,] +∞ ) ↦ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } ) )
6		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑝 𝐷 𝑥 ) = ( 𝑝 𝐷 𝑋 ) )
7		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
8	6 7	eqeqan12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝑝 𝐷 𝑥 ) = 𝑟 ↔ ( 𝑝 𝐷 𝑋 ) = 𝑅 ) )
9	8	rabbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } = { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑋 ) = 𝑅 } )
10	9	adantl	⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) ∧ ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) ) → { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑥 ) = 𝑟 } = { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑋 ) = 𝑅 } )
11		simp2	⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → 𝑋 ∈ 𝐵 )
12		simp3	⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → 𝑅 ∈ ( 0 [,] +∞ ) )
13	1	fvexi	⊢ 𝐵 ∈ V
14	13	rabex	⊢ { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑋 ) = 𝑅 } ∈ V
15	14	a1i	⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑋 ) = 𝑅 } ∈ V )
16	5 10 11 12 15	ovmpod	⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ ( 0 [,] +∞ ) ) → ( 𝑋 𝑆 𝑅 ) = { 𝑝 ∈ 𝐵 ∣ ( 𝑝 𝐷 𝑋 ) = 𝑅 } )