# Metamath Proof Explorer

## Theorem kgenval

Description: Value of the compact generator. (The "k" in kGen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenval ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)=\left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}$

### Proof

Step Hyp Ref Expression
1 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)$
2 unieq ${⊢}{j}={J}\to \bigcup {j}=\bigcup {J}$
3 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
4 3 eqcomd ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \bigcup {J}={X}$
5 2 4 sylan9eqr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {j}={J}\right)\to \bigcup {j}={X}$
6 5 pweqd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {j}={J}\right)\to 𝒫\bigcup {j}=𝒫{X}$
7 oveq1 ${⊢}{j}={J}\to {j}{↾}_{𝑡}{k}={J}{↾}_{𝑡}{k}$
8 7 eleq1d ${⊢}{j}={J}\to \left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}↔{J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)$
9 7 eleq2d ${⊢}{j}={J}\to \left({x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)↔{x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
10 8 9 imbi12d ${⊢}{j}={J}\to \left(\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)↔\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
11 10 adantl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {j}={J}\right)\to \left(\left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)↔\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
12 6 11 raleqbidv ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {j}={J}\right)\to \left(\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)↔\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
13 6 12 rabeqbidv ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {j}={J}\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\}=\left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}$
14 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
15 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
16 pwexg ${⊢}{X}\in {J}\to 𝒫{X}\in \mathrm{V}$
17 rabexg ${⊢}𝒫{X}\in \mathrm{V}\to \left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}\in \mathrm{V}$
18 15 16 17 3syl ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}\in \mathrm{V}$
19 1 13 14 18 fvmptd2 ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)=\left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}$