# Metamath Proof Explorer

## Definition df-kgen

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. ( kGenj ) , iff the preimage of x is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion df-kgen ${⊢}\mathrm{𝑘Gen}=\left({j}\in \mathrm{Top}⟼\left\{{x}\in 𝒫\bigcup {j}|\forall {k}\in 𝒫\bigcup {j}\phantom{\rule{.4em}{0ex}}\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ckgen ${class}\mathrm{𝑘Gen}$
1 vj ${setvar}{j}$
2 ctop ${class}\mathrm{Top}$
3 vx ${setvar}{x}$
4 1 cv ${setvar}{j}$
5 4 cuni ${class}\bigcup {j}$
6 5 cpw ${class}𝒫\bigcup {j}$
7 vk ${setvar}{k}$
8 crest ${class}{↾}_{𝑡}$
9 7 cv ${setvar}{k}$
10 4 9 8 co ${class}\left({j}{↾}_{𝑡}{k}\right)$
11 ccmp ${class}\mathrm{Comp}$
12 10 11 wcel ${wff}{j}{↾}_{𝑡}{k}\in \mathrm{Comp}$
13 3 cv ${setvar}{x}$
14 13 9 cin ${class}\left({x}\cap {k}\right)$
15 14 10 wcel ${wff}{x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)$
16 12 15 wi ${wff}\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)$
17 16 7 6 wral ${wff}\forall {k}\in 𝒫\bigcup {j}\phantom{\rule{.4em}{0ex}}\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)$
18 17 3 6 crab ${class}\left\{{x}\in 𝒫\bigcup {j}|\forall {k}\in 𝒫\bigcup {j}\phantom{\rule{.4em}{0ex}}\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)\right\}$
19 1 2 18 cmpt ${class}\left({j}\in \mathrm{Top}⟼\left\{{x}\in 𝒫\bigcup {j}|\forall {k}\in 𝒫\bigcup {j}\phantom{\rule{.4em}{0ex}}\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)\right\}\right)$
20 0 19 wceq ${wff}\mathrm{𝑘Gen}=\left({j}\in \mathrm{Top}⟼\left\{{x}\in 𝒫\bigcup {j}|\forall {k}\in 𝒫\bigcup {j}\phantom{\rule{.4em}{0ex}}\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)\right\}\right)$