Detailed syntax breakdown of Definition df-hcmp
Step | Hyp | Ref
| Expression |
1 | | chcmp 31412 |
. 2
class
HCmp |
2 | | vu |
. . . . . . 7
setvar 𝑢 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑢 |
4 | | cust 22885 |
. . . . . . . 8
class
UnifOn |
5 | 4 | crn 5518 |
. . . . . . 7
class ran
UnifOn |
6 | 5 | cuni 4791 |
. . . . . 6
class ∪ ran UnifOn |
7 | 3, 6 | wcel 2112 |
. . . . 5
wff 𝑢 ∈ ∪ ran UnifOn |
8 | | vw |
. . . . . . 7
setvar 𝑤 |
9 | 8 | cv 1538 |
. . . . . 6
class 𝑤 |
10 | | ccusp 22983 |
. . . . . 6
class
CUnifSp |
11 | 9, 10 | wcel 2112 |
. . . . 5
wff 𝑤 ∈ CUnifSp |
12 | 7, 11 | wa 400 |
. . . 4
wff (𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) |
13 | | cuss 22939 |
. . . . . . 7
class
UnifSt |
14 | 9, 13 | cfv 6328 |
. . . . . 6
class
(UnifSt‘𝑤) |
15 | 3 | cuni 4791 |
. . . . . . 7
class ∪ 𝑢 |
16 | 15 | cdm 5517 |
. . . . . 6
class dom ∪ 𝑢 |
17 | | crest 16737 |
. . . . . 6
class
↾t |
18 | 14, 16, 17 | co 7143 |
. . . . 5
class
((UnifSt‘𝑤)
↾t dom ∪ 𝑢) |
19 | 18, 3 | wceq 1539 |
. . . 4
wff
((UnifSt‘𝑤)
↾t dom ∪ 𝑢) = 𝑢 |
20 | | ctopn 16738 |
. . . . . . . 8
class
TopOpen |
21 | 9, 20 | cfv 6328 |
. . . . . . 7
class
(TopOpen‘𝑤) |
22 | | ccl 21703 |
. . . . . . 7
class
cls |
23 | 21, 22 | cfv 6328 |
. . . . . 6
class
(cls‘(TopOpen‘𝑤)) |
24 | 16, 23 | cfv 6328 |
. . . . 5
class
((cls‘(TopOpen‘𝑤))‘dom ∪
𝑢) |
25 | | cbs 16526 |
. . . . . 6
class
Base |
26 | 9, 25 | cfv 6328 |
. . . . 5
class
(Base‘𝑤) |
27 | 24, 26 | wceq 1539 |
. . . 4
wff
((cls‘(TopOpen‘𝑤))‘dom ∪
𝑢) = (Base‘𝑤) |
28 | 12, 19, 27 | w3a 1085 |
. . 3
wff ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) =
𝑢 ∧
((cls‘(TopOpen‘𝑤))‘dom ∪
𝑢) = (Base‘𝑤)) |
29 | 28, 2, 8 | copab 5087 |
. 2
class
{〈𝑢, 𝑤〉 ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) =
𝑢 ∧
((cls‘(TopOpen‘𝑤))‘dom ∪
𝑢) = (Base‘𝑤))} |
30 | 1, 29 | wceq 1539 |
1
wff HCmp =
{〈𝑢, 𝑤〉 ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) =
𝑢 ∧
((cls‘(TopOpen‘𝑤))‘dom ∪
𝑢) = (Base‘𝑤))} |