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 )