Metamath Proof Explorer

Theorem kgenidm

Description: The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenidm ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \mathrm{𝑘Gen}\left({J}\right)={J}$

Proof

Step Hyp Ref Expression
1 kgenf ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$
2 ffn ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}\to \mathrm{𝑘Gen}Fn\mathrm{Top}$
3 fvelrnb ${⊢}\mathrm{𝑘Gen}Fn\mathrm{Top}\to \left({J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\exists {j}\in \mathrm{Top}\phantom{\rule{.4em}{0ex}}\mathrm{𝑘Gen}\left({j}\right)={J}\right)$
4 1 2 3 mp2b ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\exists {j}\in \mathrm{Top}\phantom{\rule{.4em}{0ex}}\mathrm{𝑘Gen}\left({j}\right)={J}$
5 toptopon2 ${⊢}{j}\in \mathrm{Top}↔{j}\in \mathrm{TopOn}\left(\bigcup {j}\right)$
6 kgentopon ${⊢}{j}\in \mathrm{TopOn}\left(\bigcup {j}\right)\to \mathrm{𝑘Gen}\left({j}\right)\in \mathrm{TopOn}\left(\bigcup {j}\right)$
7 5 6 sylbi ${⊢}{j}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left({j}\right)\in \mathrm{TopOn}\left(\bigcup {j}\right)$
8 kgentopon ${⊢}\mathrm{𝑘Gen}\left({j}\right)\in \mathrm{TopOn}\left(\bigcup {j}\right)\to \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\in \mathrm{TopOn}\left(\bigcup {j}\right)$
9 7 8 syl ${⊢}{j}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\in \mathrm{TopOn}\left(\bigcup {j}\right)$
10 toponss ${⊢}\left(\mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\in \mathrm{TopOn}\left(\bigcup {j}\right)\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to {x}\subseteq \bigcup {j}$
11 9 10 sylan ${⊢}\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to {x}\subseteq \bigcup {j}$
12 simplr ${⊢}\left(\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\wedge \left({k}\in 𝒫\bigcup {j}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)$
13 kgencmp2 ${⊢}{j}\in \mathrm{Top}\to \left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}↔\mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}\in \mathrm{Comp}\right)$
14 13 biimpa ${⊢}\left({j}\in \mathrm{Top}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}\in \mathrm{Comp}$
15 14 ad2ant2rl ${⊢}\left(\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\wedge \left({k}\in 𝒫\bigcup {j}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to \mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}\in \mathrm{Comp}$
16 kgeni ${⊢}\left({x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\wedge \mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {x}\cap {k}\in \left(\mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}\right)$
17 12 15 16 syl2anc ${⊢}\left(\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\wedge \left({k}\in 𝒫\bigcup {j}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {x}\cap {k}\in \left(\mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}\right)$
18 kgencmp ${⊢}\left({j}\in \mathrm{Top}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {j}{↾}_{𝑡}{k}=\mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}$
19 18 ad2ant2rl ${⊢}\left(\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\wedge \left({k}\in 𝒫\bigcup {j}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {j}{↾}_{𝑡}{k}=\mathrm{𝑘Gen}\left({j}\right){↾}_{𝑡}{k}$
20 17 19 eleqtrrd ${⊢}\left(\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\wedge \left({k}\in 𝒫\bigcup {j}\wedge {j}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)$
21 20 expr ${⊢}\left(\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\wedge {k}\in 𝒫\bigcup {j}\right)\to \left({j}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({j}{↾}_{𝑡}{k}\right)\right)$
22 21 ralrimiva ${⊢}\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to \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)$
23 simpl ${⊢}\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to {j}\in \mathrm{Top}$
24 23 5 sylib ${⊢}\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to {j}\in \mathrm{TopOn}\left(\bigcup {j}\right)$
25 elkgen ${⊢}{j}\in \mathrm{TopOn}\left(\bigcup {j}\right)\to \left({x}\in \mathrm{𝑘Gen}\left({j}\right)↔\left({x}\subseteq \bigcup {j}\wedge \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)$
26 24 25 syl ${⊢}\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to \left({x}\in \mathrm{𝑘Gen}\left({j}\right)↔\left({x}\subseteq \bigcup {j}\wedge \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)$
27 11 22 26 mpbir2and ${⊢}\left({j}\in \mathrm{Top}\wedge {x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\right)\to {x}\in \mathrm{𝑘Gen}\left({j}\right)$
28 27 ex ${⊢}{j}\in \mathrm{Top}\to \left({x}\in \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\to {x}\in \mathrm{𝑘Gen}\left({j}\right)\right)$
29 28 ssrdv ${⊢}{j}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\subseteq \mathrm{𝑘Gen}\left({j}\right)$
30 fveq2 ${⊢}\mathrm{𝑘Gen}\left({j}\right)={J}\to \mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)=\mathrm{𝑘Gen}\left({J}\right)$
31 id ${⊢}\mathrm{𝑘Gen}\left({j}\right)={J}\to \mathrm{𝑘Gen}\left({j}\right)={J}$
32 30 31 sseq12d ${⊢}\mathrm{𝑘Gen}\left({j}\right)={J}\to \left(\mathrm{𝑘Gen}\left(\mathrm{𝑘Gen}\left({j}\right)\right)\subseteq \mathrm{𝑘Gen}\left({j}\right)↔\mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$
33 29 32 syl5ibcom ${⊢}{j}\in \mathrm{Top}\to \left(\mathrm{𝑘Gen}\left({j}\right)={J}\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$
34 33 rexlimiv ${⊢}\exists {j}\in \mathrm{Top}\phantom{\rule{.4em}{0ex}}\mathrm{𝑘Gen}\left({j}\right)={J}\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}$
35 4 34 sylbi ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}$
36 kgentop ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to {J}\in \mathrm{Top}$
37 kgenss ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
38 36 37 syl ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
39 35 38 eqssd ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \mathrm{𝑘Gen}\left({J}\right)={J}$