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

Definition df-kgen 19240
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 19239 . 2  class 𝑘Gen
2 vj . . 3  setvar  j
3 ctop 18631 . . 3  class  Top
42cv 1369 . . . . . . . 8  class  j
5 vk . . . . . . . . 9  setvar  k
65cv 1369 . . . . . . . 8  class  k
7 crest 14479 . . . . . . . 8  classt
84, 6, 7co 6201 . . . . . . 7  class  ( jt  k )
9 ccmp 19122 . . . . . . 7  class  Comp
108, 9wcel 1758 . . . . . 6  wff  ( jt  k )  e.  Comp
11 vx . . . . . . . . 9  setvar  x
1211cv 1369 . . . . . . . 8  class  x
1312, 6cin 3436 . . . . . . 7  class  ( x  i^i  k )
1413, 8wcel 1758 . . . . . 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 4200 . . . . . 6  class  U. j
1716cpw 3969 . . . . 5  class  ~P U. j
1815, 5, 17wral 2799 . . . 4  wff  A. k  e.  ~P  U. j ( ( jt  k )  e. 
Comp  ->  ( x  i^i  k )  e.  ( jt  k ) )
1918, 11, 17crab 2803 . . 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 4459 . 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 1370 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 setvar class
This definition is referenced by:  kgenval  19241  kgeni  19243  kgenf  19247
  Copyright terms: Public domain W3C validator