Step | Hyp | Ref
| Expression |
1 | | cpin 24520 |
. 2
class
Οn |
2 | | vj |
. . 3
setvar π |
3 | | vp |
. . 3
setvar π |
4 | | ctop 22395 |
. . 3
class
Top |
5 | 2 | cv 1541 |
. . . 4
class π |
6 | 5 | cuni 4909 |
. . 3
class βͺ π |
7 | | vn |
. . . 4
setvar π |
8 | | cn0 12472 |
. . . 4
class
β0 |
9 | 7 | cv 1541 |
. . . . . . 7
class π |
10 | 3 | cv 1541 |
. . . . . . . 8
class π |
11 | | comn 24518 |
. . . . . . . 8
class
Ξ©π |
12 | 5, 10, 11 | co 7409 |
. . . . . . 7
class (π Ξ©π
π) |
13 | 9, 12 | cfv 6544 |
. . . . . 6
class ((π Ξ©π
π)βπ) |
14 | | c1st 7973 |
. . . . . 6
class
1st |
15 | 13, 14 | cfv 6544 |
. . . . 5
class
(1st β((π Ξ©π π)βπ)) |
16 | | cc0 11110 |
. . . . . . 7
class
0 |
17 | 9, 16 | wceq 1542 |
. . . . . 6
wff π = 0 |
18 | | vf |
. . . . . . . . . . . 12
setvar π |
19 | 18 | cv 1541 |
. . . . . . . . . . 11
class π |
20 | 16, 19 | cfv 6544 |
. . . . . . . . . 10
class (πβ0) |
21 | | vx |
. . . . . . . . . . 11
setvar π₯ |
22 | 21 | cv 1541 |
. . . . . . . . . 10
class π₯ |
23 | 20, 22 | wceq 1542 |
. . . . . . . . 9
wff (πβ0) = π₯ |
24 | | c1 11111 |
. . . . . . . . . . 11
class
1 |
25 | 24, 19 | cfv 6544 |
. . . . . . . . . 10
class (πβ1) |
26 | | vy |
. . . . . . . . . . 11
setvar π¦ |
27 | 26 | cv 1541 |
. . . . . . . . . 10
class π¦ |
28 | 25, 27 | wceq 1542 |
. . . . . . . . 9
wff (πβ1) = π¦ |
29 | 23, 28 | wa 397 |
. . . . . . . 8
wff ((πβ0) = π₯ β§ (πβ1) = π¦) |
30 | | cii 24391 |
. . . . . . . . 9
class
II |
31 | | ccn 22728 |
. . . . . . . . 9
class
Cn |
32 | 30, 5, 31 | co 7409 |
. . . . . . . 8
class (II Cn
π) |
33 | 29, 18, 32 | wrex 3071 |
. . . . . . 7
wff
βπ β (II
Cn π)((πβ0) = π₯ β§ (πβ1) = π¦) |
34 | 33, 21, 26 | copab 5211 |
. . . . . 6
class
{β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)} |
35 | | cmin 11444 |
. . . . . . . . . . 11
class
β |
36 | 9, 24, 35 | co 7409 |
. . . . . . . . . 10
class (π β 1) |
37 | 36, 12 | cfv 6544 |
. . . . . . . . 9
class ((π Ξ©π
π)β(π β 1)) |
38 | 37, 14 | cfv 6544 |
. . . . . . . 8
class
(1st β((π Ξ©π π)β(π β 1))) |
39 | | ctopn 17367 |
. . . . . . . 8
class
TopOpen |
40 | 38, 39 | cfv 6544 |
. . . . . . 7
class
(TopOpenβ(1st β((π Ξ©π π)β(π β 1)))) |
41 | | cphtpc 24485 |
. . . . . . 7
class
βph |
42 | 40, 41 | cfv 6544 |
. . . . . 6
class (
βphβ(TopOpenβ(1st β((π Ξ©π
π)β(π β 1))))) |
43 | 17, 34, 42 | cif 4529 |
. . . . 5
class if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, (
βphβ(TopOpenβ(1st β((π Ξ©π
π)β(π β
1)))))) |
44 | | cqus 17451 |
. . . . 5
class
/s |
45 | 15, 43, 44 | co 7409 |
. . . 4
class
((1st β((π Ξ©π π)βπ)) /s if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, (
βphβ(TopOpenβ(1st β((π Ξ©π
π)β(π β
1))))))) |
46 | 7, 8, 45 | cmpt 5232 |
. . 3
class (π β β0
β¦ ((1st β((π Ξ©π π)βπ)) /s if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, (
βphβ(TopOpenβ(1st β((π Ξ©π
π)β(π β
1)))))))) |
47 | 2, 3, 4, 6, 46 | cmpo 7411 |
. 2
class (π β Top, π β βͺ π β¦ (π β β0 β¦
((1st β((π
Ξ©π π)βπ)) /s if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, (
βphβ(TopOpenβ(1st β((π Ξ©π
π)β(π β
1))))))))) |
48 | 1, 47 | wceq 1542 |
1
wff
Οn = (π
β Top, π β βͺ π
β¦ (π β
β0 β¦ ((1st β((π Ξ©π π)βπ)) /s if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, (
βphβ(TopOpenβ(1st β((π Ξ©π
π)β(π β
1))))))))) |