MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-kgen Unicode version

Definition df-kgen 17245
Description: Define the "compact generator", the functor from topological spaces to compactly generated spaces. Also known as the k-ification operation. A set is k-open, i.e.  x  e.  (𝑘Gen `  j
), iff the preimage of 
x is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
Assertion
Ref Expression
df-kgen  |- 𝑘Gen  =  (
j  e.  Top  |->  { x  e.  ~P U. j  |  A. k  e.  ~P  U. j ( ( jt  k )  e. 
Comp  ->  ( x  i^i  k )  e.  ( jt  k ) ) } )
Distinct variable group:    j, k, x

Detailed syntax breakdown of Definition df-kgen
StepHypRef Expression
1 ckgen 17244 . 2  class 𝑘Gen
2 vj . . 3  set  j
3 ctop 16647 . . 3  class  Top
42cv 1631 . . . . . . . 8  class  j
5 vk . . . . . . . . 9  set  k
65cv 1631 . . . . . . . 8  class  k
7 crest 13341 . . . . . . . 8  classt
84, 6, 7co 5874 . . . . . . 7  class  ( jt  k )
9 ccmp 17129 . . . . . . 7  class  Comp
108, 9wcel 1696 . . . . . 6  wff  ( jt  k )  e.  Comp
11 vx . . . . . . . . 9  set  x
1211cv 1631 . . . . . . . 8  class  x
1312, 6cin 3164 . . . . . . 7  class  ( x  i^i  k )
1413, 8wcel 1696 . . . . . 6  wff  ( x  i^i  k )  e.  ( jt  k )
1510, 14wi 4 . . . . 5  wff  ( ( jt  k )  e.  Comp  -> 
( x  i^i  k
)  e.  ( jt  k ) )
164cuni 3843 . . . . . 6  class  U. j
1716cpw 3638 . . . . 5  class  ~P U. j
1815, 5, 17wral 2556 . . . 4  wff  A. k  e.  ~P  U. j ( ( jt  k )  e. 
Comp  ->  ( x  i^i  k )  e.  ( jt  k ) )
1918, 11, 17crab 2560 . . 3  class  { x  e.  ~P U. j  | 
A. k  e.  ~P  U. j ( ( jt  k )  e.  Comp  ->  ( x  i^i  k )  e.  ( jt  k ) ) }
202, 3, 19cmpt 4093 . 2  class  ( j  e.  Top  |->  { x  e.  ~P U. j  | 
A. k  e.  ~P  U. j ( ( jt  k )  e.  Comp  ->  ( x  i^i  k )  e.  ( jt  k ) ) } )
211, 20wceq 1632 1  wff 𝑘Gen  =  (
j  e.  Top  |->  { x  e.  ~P U. j  |  A. k  e.  ~P  U. j ( ( jt  k )  e. 
Comp  ->  ( x  i^i  k )  e.  ( jt  k ) ) } )
Colors of variables: wff set class
This definition is referenced by:  kgenval  17246  kgeni  17248  kgenf  17252
  Copyright terms: Public domain W3C validator