# Metamath Proof Explorer

## Theorem kgen2ss

Description: The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgen2ss ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to \mathrm{𝑘Gen}\left({J}\right)\subseteq \mathrm{𝑘Gen}\left({K}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 elpwi ${⊢}{k}\in 𝒫{X}\to {k}\subseteq {X}$
3 resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {k}\subseteq {X}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
4 1 2 3 syl2an ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
5 simp2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to {K}\in \mathrm{TopOn}\left({X}\right)$
6 resttopon ${⊢}\left({K}\in \mathrm{TopOn}\left({X}\right)\wedge {k}\subseteq {X}\right)\to {K}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
7 5 2 6 syl2an ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {K}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
8 toponuni ${⊢}{K}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)\to {k}=\bigcup \left({K}{↾}_{𝑡}{k}\right)$
9 7 8 syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {k}=\bigcup \left({K}{↾}_{𝑡}{k}\right)$
10 9 fveq2d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to \mathrm{TopOn}\left({k}\right)=\mathrm{TopOn}\left(\bigcup \left({K}{↾}_{𝑡}{k}\right)\right)$
11 4 10 eleqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left(\bigcup \left({K}{↾}_{𝑡}{k}\right)\right)$
12 simpl2 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {K}\in \mathrm{TopOn}\left({X}\right)$
13 topontop ${⊢}{K}\in \mathrm{TopOn}\left({X}\right)\to {K}\in \mathrm{Top}$
14 12 13 syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {K}\in \mathrm{Top}$
15 simpl3 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {J}\subseteq {K}$
16 ssrest ${⊢}\left({K}\in \mathrm{Top}\wedge {J}\subseteq {K}\right)\to {J}{↾}_{𝑡}{k}\subseteq {K}{↾}_{𝑡}{k}$
17 14 15 16 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to {J}{↾}_{𝑡}{k}\subseteq {K}{↾}_{𝑡}{k}$
18 eqid ${⊢}\bigcup \left({K}{↾}_{𝑡}{k}\right)=\bigcup \left({K}{↾}_{𝑡}{k}\right)$
19 18 sscmp ${⊢}\left({J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left(\bigcup \left({K}{↾}_{𝑡}{k}\right)\right)\wedge {K}{↾}_{𝑡}{k}\in \mathrm{Comp}\wedge {J}{↾}_{𝑡}{k}\subseteq {K}{↾}_{𝑡}{k}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
20 19 3com23 ${⊢}\left({J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left(\bigcup \left({K}{↾}_{𝑡}{k}\right)\right)\wedge {J}{↾}_{𝑡}{k}\subseteq {K}{↾}_{𝑡}{k}\wedge {K}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
21 20 3expia ${⊢}\left({J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left(\bigcup \left({K}{↾}_{𝑡}{k}\right)\right)\wedge {J}{↾}_{𝑡}{k}\subseteq {K}{↾}_{𝑡}{k}\right)\to \left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)$
22 11 17 21 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to \left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)$
23 17 sseld ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to \left({x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\to {x}\cap {k}\in \left({K}{↾}_{𝑡}{k}\right)\right)$
24 22 23 imim12d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\wedge {k}\in 𝒫{X}\right)\to \left(\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\to \left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({K}{↾}_{𝑡}{k}\right)\right)\right)$
25 24 ralimdva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\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 \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({K}{↾}_{𝑡}{k}\right)\right)\right)$
26 25 anim2d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to \left(\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)\to \left({x}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({K}{↾}_{𝑡}{k}\right)\right)\right)\right)$
27 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)$
28 27 3ad2ant1 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\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)$
29 elkgen ${⊢}{K}\in \mathrm{TopOn}\left({X}\right)\to \left({x}\in \mathrm{𝑘Gen}\left({K}\right)↔\left({x}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({K}{↾}_{𝑡}{k}\right)\right)\right)\right)$
30 29 3ad2ant2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to \left({x}\in \mathrm{𝑘Gen}\left({K}\right)↔\left({x}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({K}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({K}{↾}_{𝑡}{k}\right)\right)\right)\right)$
31 26 28 30 3imtr4d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)$
32 31 ssrdv ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to \mathrm{𝑘Gen}\left({J}\right)\subseteq \mathrm{𝑘Gen}\left({K}\right)$