# Metamath Proof Explorer

## Theorem kgencmp

Description: The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015)

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

### Proof

Step Hyp Ref Expression
1 kgenftop ${⊢}{J}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}$
2 1 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}$
3 kgenss ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
4 3 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
5 ssrest ${⊢}\left(\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}\wedge {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to {J}{↾}_{𝑡}{K}\subseteq \mathrm{𝑘Gen}\left({J}\right){↾}_{𝑡}{K}$
6 2 4 5 syl2anc ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{K}\subseteq \mathrm{𝑘Gen}\left({J}\right){↾}_{𝑡}{K}$
7 cmptop ${⊢}{J}{↾}_{𝑡}{K}\in \mathrm{Comp}\to {J}{↾}_{𝑡}{K}\in \mathrm{Top}$
8 7 adantl ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{K}\in \mathrm{Top}$
9 restrcl ${⊢}{J}{↾}_{𝑡}{K}\in \mathrm{Top}\to \left({J}\in \mathrm{V}\wedge {K}\in \mathrm{V}\right)$
10 9 simprd ${⊢}{J}{↾}_{𝑡}{K}\in \mathrm{Top}\to {K}\in \mathrm{V}$
11 8 10 syl ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {K}\in \mathrm{V}$
12 restval ${⊢}\left(\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}\wedge {K}\in \mathrm{V}\right)\to \mathrm{𝑘Gen}\left({J}\right){↾}_{𝑡}{K}=\mathrm{ran}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)⟼{x}\cap {K}\right)$
13 2 11 12 syl2anc ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \mathrm{𝑘Gen}\left({J}\right){↾}_{𝑡}{K}=\mathrm{ran}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)⟼{x}\cap {K}\right)$
14 simpr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {x}\in \mathrm{𝑘Gen}\left({J}\right)$
15 simplr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {J}{↾}_{𝑡}{K}\in \mathrm{Comp}$
16 kgeni ${⊢}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {x}\cap {K}\in \left({J}{↾}_{𝑡}{K}\right)$
17 14 15 16 syl2anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {x}\cap {K}\in \left({J}{↾}_{𝑡}{K}\right)$
18 17 fmpttd ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \left({x}\in \mathrm{𝑘Gen}\left({J}\right)⟼{x}\cap {K}\right):\mathrm{𝑘Gen}\left({J}\right)⟶{J}{↾}_{𝑡}{K}$
19 18 frnd ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \mathrm{ran}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)⟼{x}\cap {K}\right)\subseteq {J}{↾}_{𝑡}{K}$
20 13 19 eqsstrd ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to \mathrm{𝑘Gen}\left({J}\right){↾}_{𝑡}{K}\subseteq {J}{↾}_{𝑡}{K}$
21 6 20 eqssd ${⊢}\left({J}\in \mathrm{Top}\wedge {J}{↾}_{𝑡}{K}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{K}=\mathrm{𝑘Gen}\left({J}\right){↾}_{𝑡}{K}$