Step | Hyp | Ref
| Expression |
1 | | cxko 22818 |
. 2
class
βko |
2 | | vs |
. . 3
setvar π |
3 | | vr |
. . 3
setvar π |
4 | | ctop 22148 |
. . 3
class
Top |
5 | | vk |
. . . . . . 7
setvar π |
6 | | vv |
. . . . . . 7
setvar π£ |
7 | 3 | cv 1539 |
. . . . . . . . . 10
class π |
8 | | vx |
. . . . . . . . . . 11
setvar π₯ |
9 | 8 | cv 1539 |
. . . . . . . . . 10
class π₯ |
10 | | crest 17228 |
. . . . . . . . . 10
class
βΎt |
11 | 7, 9, 10 | co 7337 |
. . . . . . . . 9
class (π βΎt π₯) |
12 | | ccmp 22643 |
. . . . . . . . 9
class
Comp |
13 | 11, 12 | wcel 2105 |
. . . . . . . 8
wff (π βΎt π₯) β Comp |
14 | 7 | cuni 4852 |
. . . . . . . . 9
class βͺ π |
15 | 14 | cpw 4547 |
. . . . . . . 8
class π«
βͺ π |
16 | 13, 8, 15 | crab 3403 |
. . . . . . 7
class {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp} |
17 | 2 | cv 1539 |
. . . . . . 7
class π |
18 | | vf |
. . . . . . . . . . 11
setvar π |
19 | 18 | cv 1539 |
. . . . . . . . . 10
class π |
20 | 5 | cv 1539 |
. . . . . . . . . 10
class π |
21 | 19, 20 | cima 5623 |
. . . . . . . . 9
class (π β π) |
22 | 6 | cv 1539 |
. . . . . . . . 9
class π£ |
23 | 21, 22 | wss 3898 |
. . . . . . . 8
wff (π β π) β π£ |
24 | | ccn 22481 |
. . . . . . . . 9
class
Cn |
25 | 7, 17, 24 | co 7337 |
. . . . . . . 8
class (π Cn π ) |
26 | 23, 18, 25 | crab 3403 |
. . . . . . 7
class {π β (π Cn π ) β£ (π β π) β π£} |
27 | 5, 6, 16, 17, 26 | cmpo 7339 |
. . . . . 6
class (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π Cn π ) β£ (π β π) β π£}) |
28 | 27 | crn 5621 |
. . . . 5
class ran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π Cn π ) β£ (π β π) β π£}) |
29 | | cfi 9267 |
. . . . 5
class
fi |
30 | 28, 29 | cfv 6479 |
. . . 4
class
(fiβran (π
β {π₯ β π«
βͺ π β£ (π βΎt π₯) β Comp}, π£ β π β¦ {π β (π Cn π ) β£ (π β π) β π£})) |
31 | | ctg 17245 |
. . . 4
class
topGen |
32 | 30, 31 | cfv 6479 |
. . 3
class
(topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π Cn π ) β£ (π β π) β π£}))) |
33 | 2, 3, 4, 4, 32 | cmpo 7339 |
. 2
class (π β Top, π β Top β¦
(topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π Cn π ) β£ (π β π) β π£})))) |
34 | 1, 33 | wceq 1540 |
1
wff
βko = (π
β Top, π β Top
β¦ (topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π Cn π ) β£ (π β π) β π£})))) |