Step | Hyp | Ref
| Expression |
1 | | comi 24516 |
. 2
class
Ξ©1 |
2 | | vj |
. . 3
setvar π |
3 | | vy |
. . 3
setvar π¦ |
4 | | ctop 22394 |
. . 3
class
Top |
5 | 2 | cv 1540 |
. . . 4
class π |
6 | 5 | cuni 4908 |
. . 3
class βͺ π |
7 | | cnx 17125 |
. . . . . 6
class
ndx |
8 | | cbs 17143 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6543 |
. . . . 5
class
(Baseβndx) |
10 | | cc0 11109 |
. . . . . . . . 9
class
0 |
11 | | vf |
. . . . . . . . . 10
setvar π |
12 | 11 | cv 1540 |
. . . . . . . . 9
class π |
13 | 10, 12 | cfv 6543 |
. . . . . . . 8
class (πβ0) |
14 | 3 | cv 1540 |
. . . . . . . 8
class π¦ |
15 | 13, 14 | wceq 1541 |
. . . . . . 7
wff (πβ0) = π¦ |
16 | | c1 11110 |
. . . . . . . . 9
class
1 |
17 | 16, 12 | cfv 6543 |
. . . . . . . 8
class (πβ1) |
18 | 17, 14 | wceq 1541 |
. . . . . . 7
wff (πβ1) = π¦ |
19 | 15, 18 | wa 396 |
. . . . . 6
wff ((πβ0) = π¦ β§ (πβ1) = π¦) |
20 | | cii 24390 |
. . . . . . 7
class
II |
21 | | ccn 22727 |
. . . . . . 7
class
Cn |
22 | 20, 5, 21 | co 7408 |
. . . . . 6
class (II Cn
π) |
23 | 19, 11, 22 | crab 3432 |
. . . . 5
class {π β (II Cn π) β£ ((πβ0) = π¦ β§ (πβ1) = π¦)} |
24 | 9, 23 | cop 4634 |
. . . 4
class
β¨(Baseβndx), {π β (II Cn π) β£ ((πβ0) = π¦ β§ (πβ1) = π¦)}β© |
25 | | cplusg 17196 |
. . . . . 6
class
+g |
26 | 7, 25 | cfv 6543 |
. . . . 5
class
(+gβndx) |
27 | | cpco 24515 |
. . . . . 6
class
*π |
28 | 5, 27 | cfv 6543 |
. . . . 5
class
(*πβπ) |
29 | 26, 28 | cop 4634 |
. . . 4
class
β¨(+gβndx), (*πβπ)β© |
30 | | cts 17202 |
. . . . . 6
class
TopSet |
31 | 7, 30 | cfv 6543 |
. . . . 5
class
(TopSetβndx) |
32 | | cxko 23064 |
. . . . . 6
class
βko |
33 | 5, 20, 32 | co 7408 |
. . . . 5
class (π βko
II) |
34 | 31, 33 | cop 4634 |
. . . 4
class
β¨(TopSetβndx), (π βko
II)β© |
35 | 24, 29, 34 | ctp 4632 |
. . 3
class
{β¨(Baseβndx), {π β (II Cn π) β£ ((πβ0) = π¦ β§ (πβ1) = π¦)}β©, β¨(+gβndx),
(*πβπ)β©, β¨(TopSetβndx), (π βko
II)β©} |
36 | 2, 3, 4, 6, 35 | cmpo 7410 |
. 2
class (π β Top, π¦ β βͺ π β¦
{β¨(Baseβndx), {π
β (II Cn π) β£
((πβ0) = π¦ β§ (πβ1) = π¦)}β©, β¨(+gβndx),
(*πβπ)β©, β¨(TopSetβndx), (π βko
II)β©}) |
37 | 1, 36 | wceq 1541 |
1
wff
Ξ©1 = (π
β Top, π¦ β βͺ π
β¦ {β¨(Baseβndx), {π β (II Cn π) β£ ((πβ0) = π¦ β§ (πβ1) = π¦)}β©, β¨(+gβndx),
(*πβπ)β©, β¨(TopSetβndx), (π βko
II)β©}) |