# 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 ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$

### Proof

Step Hyp Ref Expression
1 vuniex ${⊢}\bigcup {j}\in \mathrm{V}$
2 1 pwex ${⊢}𝒫\bigcup {j}\in \mathrm{V}$
3 2 rabex ${⊢}\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\}\in \mathrm{V}$
4 3 a1i ${⊢}\left(\top \wedge {j}\in \mathrm{Top}\right)\to \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\}\in \mathrm{V}$
5 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)$
6 5 a1i ${⊢}\top \to \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)$
7 kgenftop ${⊢}{x}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left({x}\right)\in \mathrm{Top}$
8 7 adantl ${⊢}\left(\top \wedge {x}\in \mathrm{Top}\right)\to \mathrm{𝑘Gen}\left({x}\right)\in \mathrm{Top}$
9 4 6 8 fmpt2d ${⊢}\top \to \mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$
10 9 mptru ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$