Detailed syntax breakdown of Definition df-tus
Step | Hyp | Ref
| Expression |
1 | | ctus 22429 |
. 2
class
toUnifSp |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | cust 22373 |
. . . . 5
class
UnifOn |
4 | 3 | crn 5343 |
. . . 4
class ran
UnifOn |
5 | 4 | cuni 4658 |
. . 3
class ∪ ran UnifOn |
6 | | cnx 16219 |
. . . . . . 7
class
ndx |
7 | | cbs 16222 |
. . . . . . 7
class
Base |
8 | 6, 7 | cfv 6123 |
. . . . . 6
class
(Base‘ndx) |
9 | 2 | cv 1655 |
. . . . . . . 8
class 𝑢 |
10 | 9 | cuni 4658 |
. . . . . . 7
class ∪ 𝑢 |
11 | 10 | cdm 5342 |
. . . . . 6
class dom ∪ 𝑢 |
12 | 8, 11 | cop 4403 |
. . . . 5
class
〈(Base‘ndx), dom ∪ 𝑢〉 |
13 | | cunif 16315 |
. . . . . . 7
class
UnifSet |
14 | 6, 13 | cfv 6123 |
. . . . . 6
class
(UnifSet‘ndx) |
15 | 14, 9 | cop 4403 |
. . . . 5
class
〈(UnifSet‘ndx), 𝑢〉 |
16 | 12, 15 | cpr 4399 |
. . . 4
class
{〈(Base‘ndx), dom ∪ 𝑢〉,
〈(UnifSet‘ndx), 𝑢〉} |
17 | | cts 16311 |
. . . . . 6
class
TopSet |
18 | 6, 17 | cfv 6123 |
. . . . 5
class
(TopSet‘ndx) |
19 | | cutop 22404 |
. . . . . 6
class
unifTop |
20 | 9, 19 | cfv 6123 |
. . . . 5
class
(unifTop‘𝑢) |
21 | 18, 20 | cop 4403 |
. . . 4
class
〈(TopSet‘ndx), (unifTop‘𝑢)〉 |
22 | | csts 16220 |
. . . 4
class
sSet |
23 | 16, 21, 22 | co 6905 |
. . 3
class
({〈(Base‘ndx), dom ∪ 𝑢〉,
〈(UnifSet‘ndx), 𝑢〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑢)〉) |
24 | 2, 5, 23 | cmpt 4952 |
. 2
class (𝑢 ∈ ∪ ran UnifOn ↦ ({〈(Base‘ndx), dom ∪ 𝑢〉, 〈(UnifSet‘ndx), 𝑢〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑢)〉)) |
25 | 1, 24 | wceq 1656 |
1
wff toUnifSp =
(𝑢 ∈ ∪ ran UnifOn ↦ ({〈(Base‘ndx), dom ∪ 𝑢〉, 〈(UnifSet‘ndx), 𝑢〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑢)〉)) |