Metamath Proof Explorer

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 ⊢B=BaseW
spheres.l ⊢S=Sphere⁡W
spheres.d ⊢D=dist⁡W
Assertion spheres ⊢W∈V→S=x∈B,r∈0+∞⟼p∈B|pDx=r

Proof

Step Hyp Ref Expression
1 spheres.b ⊢B=BaseW
2 spheres.l ⊢S=Sphere⁡W
3 spheres.d ⊢D=dist⁡W
4 2 a1i ⊢W∈V→S=Sphere⁡W
5 df-sph ⊢Sphere=w∈V⟼x∈Basew,r∈0+∞⟼p∈Basew|pdist⁡wx=r
6 fveq2 ⊢w=W→Basew=BaseW
7 1 eqcomi ⊢BaseW=B
8 7 a1i ⊢w=W→BaseW=B
9 6 8 eqtrd ⊢w=W→Basew=B
10 eqidd ⊢w=W→0+∞=0+∞
11 fveq2 ⊢w=W→dist⁡w=dist⁡W
12 3 eqcomi ⊢dist⁡W=D
13 12 a1i ⊢w=W→dist⁡W=D
14 11 13 eqtrd ⊢w=W→dist⁡w=D
15 14 oveqd ⊢w=W→pdist⁡wx=pDx
16 15 eqeq1d ⊢w=W→pdist⁡wx=r↔pDx=r
17 9 16 rabeqbidv ⊢w=W→p∈Basew|pdist⁡wx=r=p∈B|pDx=r
18 9 10 17 mpoeq123dv ⊢w=W→x∈Basew,r∈0+∞⟼p∈Basew|pdist⁡wx=r=x∈B,r∈0+∞⟼p∈B|pDx=r
19 elex ⊢W∈V→W∈V
20 fvex ⊢BaseW∈V
21 1 20 eqeltri ⊢B∈V
22 ovex ⊢0+∞∈V
23 21 22 mpoex ⊢x∈B,r∈0+∞⟼p∈B|pDx=r∈V
24 23 a1i ⊢W∈V→x∈B,r∈0+∞⟼p∈B|pDx=r∈V
25 5 18 19 24 fvmptd3 ⊢W∈V→Sphere⁡W=x∈B,r∈0+∞⟼p∈B|pDx=r
26 4 25 eqtrd ⊢W∈V→S=x∈B,r∈0+∞⟼p∈B|pDx=r