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