Metamath Proof Explorer


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 ‘ 𝑤 ) 𝑥 ) = 𝑟 } ) )