Step | Hyp | Ref
| Expression |
1 | | ctoplnd 41584 |
. 2
class
TopLnd |
2 | | vx |
. . . . . . . 8
setvar π₯ |
3 | 2 | cv 1541 |
. . . . . . 7
class π₯ |
4 | 3 | cuni 4866 |
. . . . . 6
class βͺ π₯ |
5 | | vy |
. . . . . . . 8
setvar π¦ |
6 | 5 | cv 1541 |
. . . . . . 7
class π¦ |
7 | 6 | cuni 4866 |
. . . . . 6
class βͺ π¦ |
8 | 4, 7 | wceq 1542 |
. . . . 5
wff βͺ π₯ =
βͺ π¦ |
9 | | vz |
. . . . . . . . 9
setvar π§ |
10 | 9 | cv 1541 |
. . . . . . . 8
class π§ |
11 | | com 7803 |
. . . . . . . 8
class
Ο |
12 | | cdom 8884 |
. . . . . . . 8
class
βΌ |
13 | 10, 11, 12 | wbr 5106 |
. . . . . . 7
wff π§ βΌ
Ο |
14 | 10 | cuni 4866 |
. . . . . . . 8
class βͺ π§ |
15 | 4, 14 | wceq 1542 |
. . . . . . 7
wff βͺ π₯ =
βͺ π§ |
16 | 13, 15 | wa 397 |
. . . . . 6
wff (π§ βΌ Ο β§ βͺ π₯ =
βͺ π§) |
17 | 3 | cpw 4561 |
. . . . . 6
class π«
π₯ |
18 | 16, 9, 17 | wrex 3070 |
. . . . 5
wff
βπ§ β
π« π₯(π§ βΌ Ο β§ βͺ π₯ =
βͺ π§) |
19 | 8, 18 | wi 4 |
. . . 4
wff (βͺ π₯ =
βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ =
βͺ π§)) |
20 | 19, 5, 17 | wral 3061 |
. . 3
wff
βπ¦ β
π« π₯(βͺ π₯ =
βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ =
βͺ π§)) |
21 | | ctop 22258 |
. . 3
class
Top |
22 | 20, 2, 21 | crab 3406 |
. 2
class {π₯ β Top β£
βπ¦ β π«
π₯(βͺ π₯ =
βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ =
βͺ π§))} |
23 | 1, 22 | wceq 1542 |
1
wff TopLnd =
{π₯ β Top β£
βπ¦ β π«
π₯(βͺ π₯ =
βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ =
βͺ π§))} |