Detailed syntax breakdown of Definition df-tms
| Step | Hyp | Ref
| Expression |
| 1 | | ctms 24329 |
. 2
class
toMetSp |
| 2 | | vd |
. . 3
setvar 𝑑 |
| 3 | | cxmet 21349 |
. . . . 5
class
∞Met |
| 4 | 3 | crn 5686 |
. . . 4
class ran
∞Met |
| 5 | 4 | cuni 4907 |
. . 3
class ∪ ran ∞Met |
| 6 | | cnx 17230 |
. . . . . . 7
class
ndx |
| 7 | | cbs 17247 |
. . . . . . 7
class
Base |
| 8 | 6, 7 | cfv 6561 |
. . . . . 6
class
(Base‘ndx) |
| 9 | 2 | cv 1539 |
. . . . . . . 8
class 𝑑 |
| 10 | 9 | cdm 5685 |
. . . . . . 7
class dom 𝑑 |
| 11 | 10 | cdm 5685 |
. . . . . 6
class dom dom
𝑑 |
| 12 | 8, 11 | cop 4632 |
. . . . 5
class
〈(Base‘ndx), dom dom 𝑑〉 |
| 13 | | cds 17306 |
. . . . . . 7
class
dist |
| 14 | 6, 13 | cfv 6561 |
. . . . . 6
class
(dist‘ndx) |
| 15 | 14, 9 | cop 4632 |
. . . . 5
class
〈(dist‘ndx), 𝑑〉 |
| 16 | 12, 15 | cpr 4628 |
. . . 4
class
{〈(Base‘ndx), dom dom 𝑑〉, 〈(dist‘ndx), 𝑑〉} |
| 17 | | cts 17303 |
. . . . . 6
class
TopSet |
| 18 | 6, 17 | cfv 6561 |
. . . . 5
class
(TopSet‘ndx) |
| 19 | | cmopn 21354 |
. . . . . 6
class
MetOpen |
| 20 | 9, 19 | cfv 6561 |
. . . . 5
class
(MetOpen‘𝑑) |
| 21 | 18, 20 | cop 4632 |
. . . 4
class
〈(TopSet‘ndx), (MetOpen‘𝑑)〉 |
| 22 | | csts 17200 |
. . . 4
class
sSet |
| 23 | 16, 21, 22 | co 7431 |
. . 3
class
({〈(Base‘ndx), dom dom 𝑑〉, 〈(dist‘ndx), 𝑑〉} sSet
〈(TopSet‘ndx), (MetOpen‘𝑑)〉) |
| 24 | 2, 5, 23 | cmpt 5225 |
. 2
class (𝑑 ∈ ∪ ran ∞Met ↦ ({〈(Base‘ndx), dom dom
𝑑〉,
〈(dist‘ndx), 𝑑〉} sSet 〈(TopSet‘ndx),
(MetOpen‘𝑑)〉)) |
| 25 | 1, 24 | wceq 1540 |
1
wff toMetSp =
(𝑑 ∈ ∪ ran ∞Met ↦ ({〈(Base‘ndx), dom dom
𝑑〉,
〈(dist‘ndx), 𝑑〉} sSet 〈(TopSet‘ndx),
(MetOpen‘𝑑)〉)) |