Detailed syntax breakdown of Definition df-tus
Step | Hyp | Ref
| Expression |
1 | | ctus 22864 |
. 2
class
toUnifSp |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | cust 22808 |
. . . . 5
class
UnifOn |
4 | 3 | crn 5556 |
. . . 4
class ran
UnifOn |
5 | 4 | cuni 4838 |
. . 3
class ∪ ran UnifOn |
6 | | cnx 16480 |
. . . . . . 7
class
ndx |
7 | | cbs 16483 |
. . . . . . 7
class
Base |
8 | 6, 7 | cfv 6355 |
. . . . . 6
class
(Base‘ndx) |
9 | 2 | cv 1536 |
. . . . . . . 8
class 𝑢 |
10 | 9 | cuni 4838 |
. . . . . . 7
class ∪ 𝑢 |
11 | 10 | cdm 5555 |
. . . . . 6
class dom ∪ 𝑢 |
12 | 8, 11 | cop 4573 |
. . . . 5
class
〈(Base‘ndx), dom ∪ 𝑢〉 |
13 | | cunif 16575 |
. . . . . . 7
class
UnifSet |
14 | 6, 13 | cfv 6355 |
. . . . . 6
class
(UnifSet‘ndx) |
15 | 14, 9 | cop 4573 |
. . . . 5
class
〈(UnifSet‘ndx), 𝑢〉 |
16 | 12, 15 | cpr 4569 |
. . . 4
class
{〈(Base‘ndx), dom ∪ 𝑢〉,
〈(UnifSet‘ndx), 𝑢〉} |
17 | | cts 16571 |
. . . . . 6
class
TopSet |
18 | 6, 17 | cfv 6355 |
. . . . 5
class
(TopSet‘ndx) |
19 | | cutop 22839 |
. . . . . 6
class
unifTop |
20 | 9, 19 | cfv 6355 |
. . . . 5
class
(unifTop‘𝑢) |
21 | 18, 20 | cop 4573 |
. . . 4
class
〈(TopSet‘ndx), (unifTop‘𝑢)〉 |
22 | | csts 16481 |
. . . 4
class
sSet |
23 | 16, 21, 22 | co 7156 |
. . 3
class
({〈(Base‘ndx), dom ∪ 𝑢〉,
〈(UnifSet‘ndx), 𝑢〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑢)〉) |
24 | 2, 5, 23 | cmpt 5146 |
. 2
class (𝑢 ∈ ∪ ran UnifOn ↦ ({〈(Base‘ndx), dom ∪ 𝑢〉, 〈(UnifSet‘ndx), 𝑢〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑢)〉)) |
25 | 1, 24 | wceq 1537 |
1
wff toUnifSp =
(𝑢 ∈ ∪ ran UnifOn ↦ ({〈(Base‘ndx), dom ∪ 𝑢〉, 〈(UnifSet‘ndx), 𝑢〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑢)〉)) |