Metamath Proof Explorer


Theorem xkotop

Description: The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion xkotop
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )

Proof

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 )