Step | Hyp | Ref
| Expression |
1 | | c2ndc 22812 |
. 2
class
2ndΟ |
2 | | vx |
. . . . . . 7
setvar π₯ |
3 | 2 | cv 1541 |
. . . . . 6
class π₯ |
4 | | com 7806 |
. . . . . 6
class
Ο |
5 | | cdom 8887 |
. . . . . 6
class
βΌ |
6 | 3, 4, 5 | wbr 5109 |
. . . . 5
wff π₯ βΌ
Ο |
7 | | ctg 17327 |
. . . . . . 7
class
topGen |
8 | 3, 7 | cfv 6500 |
. . . . . 6
class
(topGenβπ₯) |
9 | | vj |
. . . . . . 7
setvar π |
10 | 9 | cv 1541 |
. . . . . 6
class π |
11 | 8, 10 | wceq 1542 |
. . . . 5
wff
(topGenβπ₯) =
π |
12 | 6, 11 | wa 397 |
. . . 4
wff (π₯ βΌ Ο β§
(topGenβπ₯) = π) |
13 | | ctb 22318 |
. . . 4
class
TopBases |
14 | 12, 2, 13 | wrex 3070 |
. . 3
wff
βπ₯ β
TopBases (π₯ βΌ Ο
β§ (topGenβπ₯) =
π) |
15 | 14, 9 | cab 2710 |
. 2
class {π β£ βπ₯ β TopBases (π₯ βΌ Ο β§
(topGenβπ₯) = π)} |
16 | 1, 15 | wceq 1542 |
1
wff
2ndΟ = {π β£ βπ₯ β TopBases (π₯ βΌ Ο β§ (topGenβπ₯) = π)} |