# Metamath Proof Explorer

## Theorem kgenss

Description: The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenss ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$

### Proof

Step Hyp Ref Expression
1 elssuni ${⊢}{x}\in {J}\to {x}\subseteq \bigcup {J}$
2 1 a1i ${⊢}{J}\in \mathrm{Top}\to \left({x}\in {J}\to {x}\subseteq \bigcup {J}\right)$
3 elrestr ${⊢}\left({J}\in \mathrm{Top}\wedge {k}\in 𝒫\bigcup {J}\wedge {x}\in {J}\right)\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
4 3 3expa ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {k}\in 𝒫\bigcup {J}\right)\wedge {x}\in {J}\right)\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
5 4 an32s ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\wedge {k}\in 𝒫\bigcup {J}\right)\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
6 5 a1d ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\wedge {k}\in 𝒫\bigcup {J}\right)\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
7 6 ralrimiva ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\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)$
8 7 ex ${⊢}{J}\in \mathrm{Top}\to \left({x}\in {J}\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)\right)$
9 2 8 jcad ${⊢}{J}\in \mathrm{Top}\to \left({x}\in {J}\to \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)$
10 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
11 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)$
12 10 11 sylbi ${⊢}{J}\in \mathrm{Top}\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)$
13 9 12 sylibrd ${⊢}{J}\in \mathrm{Top}\to \left({x}\in {J}\to {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)$
14 13 ssrdv ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$