# Metamath Proof Explorer

## Theorem kgeni

Description: Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgeni ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\cap {K}\in \left({J}{↾}_{𝑡}{K}\right)$

### Proof

Step Hyp Ref Expression
1 inass ${⊢}\left({A}\cap {K}\right)\cap \bigcup {J}={A}\cap \left({K}\cap \bigcup {J}\right)$
2 in32 ${⊢}\left({A}\cap {K}\right)\cap \bigcup {J}=\left({A}\cap \bigcup {J}\right)\cap {K}$
3 1 2 eqtr3i ${⊢}{A}\cap \left({K}\cap \bigcup {J}\right)=\left({A}\cap \bigcup {J}\right)\cap {K}$
4 df-kgen ${⊢}\mathrm{𝑘Gen}=\left({j}\in \mathrm{Top}⟼\left\{{x}\in 𝒫\bigcup {j}|\forall {y}\in 𝒫\bigcup {j}\phantom{\rule{.4em}{0ex}}\left({j}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {x}\cap {y}\in \left({j}{↾}_{𝑡}{y}\right)\right)\right\}\right)$
5 4 mptrcl ${⊢}{A}\in \mathrm{𝑘Gen}\left({J}\right)\to {J}\in \mathrm{Top}$
6 5 adantr ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}\in \mathrm{Top}$
7 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
8 6 7 sylib ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
9 simpl ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\in \mathrm{𝑘Gen}\left({J}\right)$
10 elkgen ${⊢}{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\to \left({A}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({A}\subseteq \bigcup {J}\wedge \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {A}\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)\right)\right)$
11 10 biimpa ${⊢}\left({J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\wedge {A}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \left({A}\subseteq \bigcup {J}\wedge \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {A}\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)\right)$
12 8 9 11 syl2anc ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \left({A}\subseteq \bigcup {J}\wedge \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {A}\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)\right)$
13 12 simpld ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\subseteq \bigcup {J}$
14 df-ss ${⊢}{A}\subseteq \bigcup {J}↔{A}\cap \bigcup {J}={A}$
15 13 14 sylib ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\cap \bigcup {J}={A}$
16 15 ineq1d ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \left({A}\cap \bigcup {J}\right)\cap {K}={A}\cap {K}$
17 3 16 syl5eq ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\cap \left({K}\cap \bigcup {J}\right)={A}\cap {K}$
18 cmptop ${⊢}{J}{↾}_{𝑡}{K}\in \mathrm{Comp}\to {J}{↾}_{𝑡}{K}\in \mathrm{Top}$
19 18 adantl ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{K}\in \mathrm{Top}$
20 restrcl ${⊢}{J}{↾}_{𝑡}{K}\in \mathrm{Top}\to \left({J}\in \mathrm{V}\wedge {K}\in \mathrm{V}\right)$
21 20 simprd ${⊢}{J}{↾}_{𝑡}{K}\in \mathrm{Top}\to {K}\in \mathrm{V}$
22 19 21 syl ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {K}\in \mathrm{V}$
23 eqid ${⊢}\bigcup {J}=\bigcup {J}$
24 23 restin ${⊢}\left({J}\in \mathrm{Top}\wedge {K}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{K}={J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)$
25 6 22 24 syl2anc ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{K}={J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)$
26 simpr ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{K}\in \mathrm{Comp}$
27 25 26 eqeltrrd ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\in \mathrm{Comp}$
28 oveq2 ${⊢}{y}={K}\cap \bigcup {J}\to {J}{↾}_{𝑡}{y}={J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)$
29 28 eleq1d ${⊢}{y}={K}\cap \bigcup {J}\to \left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}↔{J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\in \mathrm{Comp}\right)$
30 ineq2 ${⊢}{y}={K}\cap \bigcup {J}\to {A}\cap {y}={A}\cap \left({K}\cap \bigcup {J}\right)$
31 30 28 eleq12d ${⊢}{y}={K}\cap \bigcup {J}\to \left({A}\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)↔{A}\cap \left({K}\cap \bigcup {J}\right)\in \left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\right)\right)$
32 29 31 imbi12d ${⊢}{y}={K}\cap \bigcup {J}\to \left(\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {A}\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)↔\left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\in \mathrm{Comp}\to {A}\cap \left({K}\cap \bigcup {J}\right)\in \left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\right)\right)\right)$
33 12 simprd ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {A}\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)$
34 inss2 ${⊢}{K}\cap \bigcup {J}\subseteq \bigcup {J}$
35 inex1g ${⊢}{K}\in \mathrm{V}\to {K}\cap \bigcup {J}\in \mathrm{V}$
36 elpwg ${⊢}{K}\cap \bigcup {J}\in \mathrm{V}\to \left({K}\cap \bigcup {J}\in 𝒫\bigcup {J}↔{K}\cap \bigcup {J}\subseteq \bigcup {J}\right)$
37 22 35 36 3syl ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \left({K}\cap \bigcup {J}\in 𝒫\bigcup {J}↔{K}\cap \bigcup {J}\subseteq \bigcup {J}\right)$
38 34 37 mpbiri ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {K}\cap \bigcup {J}\in 𝒫\bigcup {J}$
39 32 33 38 rspcdva ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\in \mathrm{Comp}\to {A}\cap \left({K}\cap \bigcup {J}\right)\in \left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\right)\right)$
40 27 39 mpd ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\cap \left({K}\cap \bigcup {J}\right)\in \left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\right)$
41 17 40 eqeltrrd ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\cap {K}\in \left({J}{↾}_{𝑡}\left({K}\cap \bigcup {J}\right)\right)$
42 41 25 eleqtrrd ${⊢}\left({A}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {A}\cap {K}\in \left({J}{↾}_{𝑡}{K}\right)$