# Metamath Proof Explorer

## Theorem elkgen

Description: Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion elkgen ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({A}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({A}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 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\}$
2 1 eleq2d ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({A}\in \mathrm{𝑘Gen}\left({J}\right)↔{A}\in \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\}\right)$
3 ineq1 ${⊢}{x}={A}\to {x}\cap {k}={A}\cap {k}$
4 3 eleq1d ${⊢}{x}={A}\to \left({x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)↔{A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
5 4 imbi2d ${⊢}{x}={A}\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 {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
6 5 ralbidv ${⊢}{x}={A}\to \left(\forall {k}\in 𝒫{X}\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 {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
7 6 elrab ${⊢}{A}\in \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\}↔\left({A}\in 𝒫{X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
8 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
9 elpw2g ${⊢}{X}\in {J}\to \left({A}\in 𝒫{X}↔{A}\subseteq {X}\right)$
10 8 9 syl ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({A}\in 𝒫{X}↔{A}\subseteq {X}\right)$
11 10 anbi1d ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left(\left({A}\in 𝒫{X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)↔\left({A}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
12 7 11 syl5bb ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({A}\in \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\}↔\left({A}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
13 2 12 bitrd ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({A}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({A}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {A}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$