Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. R = U. R |
2 |
|
eqid |
|- { x e. ~P U. R | ( R |`t x ) e. Comp } = { x e. ~P U. R | ( R |`t x ) e. Comp } |
3 |
|
eqid |
|- ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) = ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) |
4 |
1 2 3
|
xkoval |
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) ) ) |
5 |
|
fibas |
|- ( fi ` ran ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) e. TopBases |
6 |
|
tgcl |
|- ( ( fi ` ran ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) e. TopBases -> ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) ) e. Top ) |
7 |
5 6
|
ax-mp |
|- ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R | ( R |`t x ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) ) e. Top |
8 |
4 7
|
eqeltrdi |
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top ) |