Metamath Proof Explorer

Theorem kgenf

Description: The compact generator is a function on topologies. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenf 
|- kGen : Top --> Top

Proof

Step Hyp Ref Expression
1 vuniex 
 |-  U. j e. _V
2 1 pwex 
 |-  ~P U. j e. _V
3 2 rabex 
 |-  { x e. ~P U. j | A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) } e. _V
4 3 a1i 
 |-  ( ( T. /\ j e. Top ) -> { x e. ~P U. j | A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) } e. _V )
5 df-kgen 
 |-  kGen = ( j e. Top |-> { x e. ~P U. j | A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) } )
6 5 a1i 
 |-  ( T. -> kGen = ( j e. Top |-> { x e. ~P U. j | A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) } ) )
7 kgenftop 
 |-  ( x e. Top -> ( kGen ` x ) e. Top )
8 7 adantl 
 |-  ( ( T. /\ x e. Top ) -> ( kGen ` x ) e. Top )
9 4 6 8 fmpt2d 
 |-  ( T. -> kGen : Top --> Top )
10 9 mptru 
 |-  kGen : Top --> Top