Step |
Hyp |
Ref |
Expression |
0 |
|
ctsu |
|- tsums |
1 |
|
vw |
|- w |
2 |
|
cvv |
|- _V |
3 |
|
vf |
|- f |
4 |
3
|
cv |
|- f |
5 |
4
|
cdm |
|- dom f |
6 |
5
|
cpw |
|- ~P dom f |
7 |
|
cfn |
|- Fin |
8 |
6 7
|
cin |
|- ( ~P dom f i^i Fin ) |
9 |
|
vs |
|- s |
10 |
|
ctopn |
|- TopOpen |
11 |
1
|
cv |
|- w |
12 |
11 10
|
cfv |
|- ( TopOpen ` w ) |
13 |
|
cflf |
|- fLimf |
14 |
9
|
cv |
|- s |
15 |
|
cfg |
|- filGen |
16 |
|
vz |
|- z |
17 |
|
vy |
|- y |
18 |
16
|
cv |
|- z |
19 |
17
|
cv |
|- y |
20 |
18 19
|
wss |
|- z C_ y |
21 |
20 17 14
|
crab |
|- { y e. s | z C_ y } |
22 |
16 14 21
|
cmpt |
|- ( z e. s |-> { y e. s | z C_ y } ) |
23 |
22
|
crn |
|- ran ( z e. s |-> { y e. s | z C_ y } ) |
24 |
14 23 15
|
co |
|- ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) |
25 |
12 24 13
|
co |
|- ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) |
26 |
|
cgsu |
|- gsum |
27 |
4 19
|
cres |
|- ( f |` y ) |
28 |
11 27 26
|
co |
|- ( w gsum ( f |` y ) ) |
29 |
17 14 28
|
cmpt |
|- ( y e. s |-> ( w gsum ( f |` y ) ) ) |
30 |
29 25
|
cfv |
|- ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) |
31 |
9 8 30
|
csb |
|- [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) |
32 |
1 3 2 2 31
|
cmpo |
|- ( w e. _V , f e. _V |-> [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) ) |
33 |
0 32
|
wceq |
|- tsums = ( w e. _V , f e. _V |-> [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) ) |