# Metamath Proof Explorer

## Theorem iskgen3

Description: Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of X that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypothesis iskgen3.1 ${⊢}{X}=\bigcup {J}$
Assertion iskgen3 ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\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)\to {x}\in {J}\right)\right)$

### Proof

Step Hyp Ref Expression
1 iskgen3.1 ${⊢}{X}=\bigcup {J}$
2 iskgen2 ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$
3 1 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left({X}\right)$
4 elkgen ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({x}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({x}\subseteq {X}\wedge \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)$
5 3 4 sylbi ${⊢}{J}\in \mathrm{Top}\to \left({x}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({x}\subseteq {X}\wedge \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)$
6 vex ${⊢}{x}\in \mathrm{V}$
7 6 elpw ${⊢}{x}\in 𝒫{X}↔{x}\subseteq {X}$
8 7 anbi1i ${⊢}\left({x}\in 𝒫{X}\wedge \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({x}\subseteq {X}\wedge \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)$
9 5 8 syl6bbr ${⊢}{J}\in \mathrm{Top}\to \left({x}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({x}\in 𝒫{X}\wedge \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)$
10 9 imbi1d ${⊢}{J}\in \mathrm{Top}\to \left(\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\in {J}\right)↔\left(\left({x}\in 𝒫{X}\wedge \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)\to {x}\in {J}\right)\right)$
11 impexp ${⊢}\left(\left({x}\in 𝒫{X}\wedge \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)\to {x}\in {J}\right)↔\left({x}\in 𝒫{X}\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)\to {x}\in {J}\right)\right)$
12 10 11 syl6bb ${⊢}{J}\in \mathrm{Top}\to \left(\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\in {J}\right)↔\left({x}\in 𝒫{X}\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)\to {x}\in {J}\right)\right)\right)$
13 12 albidv ${⊢}{J}\in \mathrm{Top}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\in {J}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in 𝒫{X}\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)\to {x}\in {J}\right)\right)\right)$
14 dfss2 ${⊢}\mathrm{𝑘Gen}\left({J}\right)\subseteq {J}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\in {J}\right)$
15 df-ral ${⊢}\forall {x}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\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)\to {x}\in {J}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in 𝒫{X}\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)\to {x}\in {J}\right)\right)$
16 13 14 15 3bitr4g ${⊢}{J}\in \mathrm{Top}\to \left(\mathrm{𝑘Gen}\left({J}\right)\subseteq {J}↔\forall {x}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\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)\to {x}\in {J}\right)\right)$
17 16 pm5.32i ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\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)\to {x}\in {J}\right)\right)$
18 2 17 bitri ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\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)\to {x}\in {J}\right)\right)$