Step | Hyp | Ref
| Expression |
1 | | cflim 23658 |
. 2
class
fLim |
2 | | vj |
. . 3
setvar π |
3 | | vf |
. . 3
setvar π |
4 | | ctop 22615 |
. . 3
class
Top |
5 | | cfil 23569 |
. . . . 5
class
Fil |
6 | 5 | crn 5677 |
. . . 4
class ran
Fil |
7 | 6 | cuni 4908 |
. . 3
class βͺ ran Fil |
8 | | vx |
. . . . . . . . 9
setvar π₯ |
9 | 8 | cv 1540 |
. . . . . . . 8
class π₯ |
10 | 9 | csn 4628 |
. . . . . . 7
class {π₯} |
11 | 2 | cv 1540 |
. . . . . . . 8
class π |
12 | | cnei 22821 |
. . . . . . . 8
class
nei |
13 | 11, 12 | cfv 6543 |
. . . . . . 7
class
(neiβπ) |
14 | 10, 13 | cfv 6543 |
. . . . . 6
class
((neiβπ)β{π₯}) |
15 | 3 | cv 1540 |
. . . . . 6
class π |
16 | 14, 15 | wss 3948 |
. . . . 5
wff
((neiβπ)β{π₯}) β π |
17 | 11 | cuni 4908 |
. . . . . . 7
class βͺ π |
18 | 17 | cpw 4602 |
. . . . . 6
class π«
βͺ π |
19 | 15, 18 | wss 3948 |
. . . . 5
wff π β π« βͺ π |
20 | 16, 19 | wa 396 |
. . . 4
wff
(((neiβπ)β{π₯}) β π β§ π β π« βͺ π) |
21 | 20, 8, 17 | crab 3432 |
. . 3
class {π₯ β βͺ π
β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)} |
22 | 2, 3, 4, 7, 21 | cmpo 7413 |
. 2
class (π β Top, π β βͺ ran Fil
β¦ {π₯ β βͺ π
β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)}) |
23 | 1, 22 | wceq 1541 |
1
wff fLim =
(π β Top, π β βͺ ran Fil β¦ {π₯ β βͺ π β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)}) |