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

Definition df-kgen 17566
 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. 𝑘Gen, iff the preimage of is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
Assertion
Ref Expression
df-kgen 𝑘Gen t t
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-kgen
StepHypRef Expression
1 ckgen 17565 . 2 𝑘Gen
2 vj . . 3
3 ctop 16958 . . 3
42cv 1651 . . . . . . . 8
5 vk . . . . . . . . 9
65cv 1651 . . . . . . . 8
7 crest 13648 . . . . . . . 8 t
84, 6, 7co 6081 . . . . . . 7 t
9 ccmp 17449 . . . . . . 7
108, 9wcel 1725 . . . . . 6 t
11 vx . . . . . . . . 9
1211cv 1651 . . . . . . . 8
1312, 6cin 3319 . . . . . . 7
1413, 8wcel 1725 . . . . . 6 t
1510, 14wi 4 . . . . 5 t t
164cuni 4015 . . . . . 6
1716cpw 3799 . . . . 5
1815, 5, 17wral 2705 . . . 4 t t
1918, 11, 17crab 2709 . . 3 t t
202, 3, 19cmpt 4266 . 2 t t
211, 20wceq 1652 1 𝑘Gen t t
 Colors of variables: wff set class This definition is referenced by:  kgenval  17567  kgeni  17569  kgenf  17573
 Copyright terms: Public domain W3C validator