Step | Hyp | Ref
| Expression |
1 | | ctms 13808 |
. 2
class
toMetSp |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cxmet 13410 |
. . . . 5
class
∞Met |
4 | 3 | crn 4627 |
. . . 4
class ran
∞Met |
5 | 4 | cuni 3809 |
. . 3
class ∪ ran ∞Met |
6 | | cnx 12458 |
. . . . . . 7
class
ndx |
7 | | cbs 12461 |
. . . . . . 7
class
Base |
8 | 6, 7 | cfv 5216 |
. . . . . 6
class
(Base‘ndx) |
9 | 2 | cv 1352 |
. . . . . . . 8
class 𝑑 |
10 | 9 | cdm 4626 |
. . . . . . 7
class dom 𝑑 |
11 | 10 | cdm 4626 |
. . . . . 6
class dom dom
𝑑 |
12 | 8, 11 | cop 3595 |
. . . . 5
class
⟨(Base‘ndx), dom dom 𝑑⟩ |
13 | | cds 12544 |
. . . . . . 7
class
dist |
14 | 6, 13 | cfv 5216 |
. . . . . 6
class
(dist‘ndx) |
15 | 14, 9 | cop 3595 |
. . . . 5
class
⟨(dist‘ndx), 𝑑⟩ |
16 | 12, 15 | cpr 3593 |
. . . 4
class
{⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} |
17 | | cts 12541 |
. . . . . 6
class
TopSet |
18 | 6, 17 | cfv 5216 |
. . . . 5
class
(TopSet‘ndx) |
19 | | cmopn 13415 |
. . . . . 6
class
MetOpen |
20 | 9, 19 | cfv 5216 |
. . . . 5
class
(MetOpen‘𝑑) |
21 | 18, 20 | cop 3595 |
. . . 4
class
⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩ |
22 | | csts 12459 |
. . . 4
class
sSet |
23 | 16, 21, 22 | co 5874 |
. . 3
class
({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet
⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩) |
24 | 2, 5, 23 | cmpt 4064 |
. 2
class (𝑑 ∈ ∪ ran ∞Met ↦ ({⟨(Base‘ndx), dom dom
𝑑⟩,
⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx),
(MetOpen‘𝑑)⟩)) |
25 | 1, 24 | wceq 1353 |
1
wff toMetSp =
(𝑑 ∈ ∪ ran ∞Met ↦ ({⟨(Base‘ndx), dom dom
𝑑⟩,
⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx),
(MetOpen‘𝑑)⟩)) |