Step |
Hyp |
Ref |
Expression |
0 |
|
cflim |
|- fLim |
1 |
|
vj |
|- j |
2 |
|
ctop |
|- Top |
3 |
|
vf |
|- f |
4 |
|
cfil |
|- Fil |
5 |
4
|
crn |
|- ran Fil |
6 |
5
|
cuni |
|- U. ran Fil |
7 |
|
vx |
|- x |
8 |
1
|
cv |
|- j |
9 |
8
|
cuni |
|- U. j |
10 |
|
cnei |
|- nei |
11 |
8 10
|
cfv |
|- ( nei ` j ) |
12 |
7
|
cv |
|- x |
13 |
12
|
csn |
|- { x } |
14 |
13 11
|
cfv |
|- ( ( nei ` j ) ` { x } ) |
15 |
3
|
cv |
|- f |
16 |
14 15
|
wss |
|- ( ( nei ` j ) ` { x } ) C_ f |
17 |
9
|
cpw |
|- ~P U. j |
18 |
15 17
|
wss |
|- f C_ ~P U. j |
19 |
16 18
|
wa |
|- ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) |
20 |
19 7 9
|
crab |
|- { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } |
21 |
1 3 2 6 20
|
cmpo |
|- ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } ) |
22 |
0 21
|
wceq |
|- fLim = ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } ) |