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 | |
|
spheres.l | |
||
spheres.d | |
||
Assertion | spheres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spheres.b | |
|
2 | spheres.l | |
|
3 | spheres.d | |
|
4 | 2 | a1i | |
5 | df-sph | |
|
6 | fveq2 | |
|
7 | 1 | eqcomi | |
8 | 7 | a1i | |
9 | 6 8 | eqtrd | |
10 | eqidd | |
|
11 | fveq2 | |
|
12 | 3 | eqcomi | |
13 | 12 | a1i | |
14 | 11 13 | eqtrd | |
15 | 14 | oveqd | |
16 | 15 | eqeq1d | |
17 | 9 16 | rabeqbidv | |
18 | 9 10 17 | mpoeq123dv | |
19 | elex | |
|
20 | fvex | |
|
21 | 1 20 | eqeltri | |
22 | ovex | |
|
23 | 21 22 | mpoex | |
24 | 23 | a1i | |
25 | 5 18 19 24 | fvmptd3 | |
26 | 4 25 | eqtrd | |