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 = w ∈ V ⟼ x ∈ Base w , r ∈ 0 +∞ ⟼ p ∈ Base w | p dist ⁡ w x = r

Detailed syntax breakdown

Step Hyp Ref Expression
0 csph class Sphere
1 vw setvar w
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 vr setvar r
8 cc0 class 0
9 cicc class .
10 cpnf class +∞
11 8 10 9 co class 0 +∞
12 vp setvar p
13 12 cv setvar p
14 cds class dist
15 5 14 cfv class dist ⁡ w
16 3 cv setvar x
17 13 16 15 co class p dist ⁡ w x
18 7 cv setvar r
19 17 18 wceq wff p dist ⁡ w x = r
20 19 12 6 crab class p ∈ Base w | p dist ⁡ w x = r
21 3 7 6 11 20 cmpo class x ∈ Base w , r ∈ 0 +∞ ⟼ p ∈ Base w | p dist ⁡ w x = r
22 1 2 21 cmpt class w ∈ V ⟼ x ∈ Base w , r ∈ 0 +∞ ⟼ p ∈ Base w | p dist ⁡ w x = r
23 0 22 wceq wff Sphere = w ∈ V ⟼ x ∈ Base w , r ∈ 0 +∞ ⟼ p ∈ Base w | p dist ⁡ w x = r