Metamath Proof Explorer

Theorem xkoval

Description: Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses xkoval.x 
|- X = U. R
xkoval.k 
|- K = { x e. ~P X | ( R |`t x ) e. Comp }
xkoval.t 
|- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )
Assertion xkoval 
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran T ) ) )

Proof

Step Hyp Ref Expression
1 xkoval.x 
 |-  X = U. R
2 xkoval.k 
 |-  K = { x e. ~P X | ( R |`t x ) e. Comp }
3 xkoval.t 
 |-  T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )
4 simpr 
 |-  ( ( s = S /\ r = R ) -> r = R )
5 4 unieqd 
 |-  ( ( s = S /\ r = R ) -> U. r = U. R )
6 5 1 eqtr4di 
 |-  ( ( s = S /\ r = R ) -> U. r = X )
7 6 pweqd 
 |-  ( ( s = S /\ r = R ) -> ~P U. r = ~P X )
8 4 oveq1d 
 |-  ( ( s = S /\ r = R ) -> ( r |`t x ) = ( R |`t x ) )
9 8 eleq1d 
 |-  ( ( s = S /\ r = R ) -> ( ( r |`t x ) e. Comp <-> ( R |`t x ) e. Comp ) )
10 7 9 rabeqbidv 
 |-  ( ( s = S /\ r = R ) -> { x e. ~P U. r | ( r |`t x ) e. Comp } = { x e. ~P X | ( R |`t x ) e. Comp } )
11 10 2 eqtr4di 
 |-  ( ( s = S /\ r = R ) -> { x e. ~P U. r | ( r |`t x ) e. Comp } = K )
12 simpl 
 |-  ( ( s = S /\ r = R ) -> s = S )
13 4 12 oveq12d 
 |-  ( ( s = S /\ r = R ) -> ( r Cn s ) = ( R Cn S ) )
14 13 rabeqdv 
 |-  ( ( s = S /\ r = R ) -> { f e. ( r Cn s ) | ( f " k ) C_ v } = { f e. ( R Cn S ) | ( f " k ) C_ v } )
15 11 12 14 mpoeq123dv 
 |-  ( ( s = S /\ r = R ) -> ( 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. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
16 15 3 eqtr4di 
 |-  ( ( s = S /\ r = R ) -> ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) = T )
17 16 rneqd 
 |-  ( ( s = S /\ r = R ) -> 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 } ) = ran T )
18 17 fveq2d 
 |-  ( ( s = S /\ r = R ) -> ( 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 } ) ) = ( fi ` ran T ) )
19 18 fveq2d 
 |-  ( ( s = S /\ r = 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 } ) ) ) = ( topGen ` ( fi ` ran T ) ) )
20 df-xko 
 |-  ^ko = ( s e. Top , r e. Top |-> ( 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 } ) ) ) )
21 fvex 
 |-  ( topGen ` ( fi ` ran T ) ) e. _V
22 19 20 21 ovmpoa 
 |-  ( ( S e. Top /\ R e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran T ) ) )
23 22 ancoms 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran T ) ) )