# Metamath Proof Explorer

## Theorem kgencn3

Description: The set of continuous functions from J to K is unaffected by k-ification of K , if J is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgencn3 ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {J}\mathrm{Cn}{K}={J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {J}=\bigcup {J}$
2 eqid ${⊢}\bigcup {K}=\bigcup {K}$
3 1 2 cnf ${⊢}{f}\in \left({J}\mathrm{Cn}{K}\right)\to {f}:\bigcup {J}⟶\bigcup {K}$
4 3 adantl ${⊢}\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\to {f}:\bigcup {J}⟶\bigcup {K}$
5 cnvimass ${⊢}{{f}}^{-1}\left[{x}\right]\subseteq \mathrm{dom}{f}$
6 4 fdmd ${⊢}\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\to \mathrm{dom}{f}=\bigcup {J}$
7 6 adantr ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to \mathrm{dom}{f}=\bigcup {J}$
8 5 7 sseqtrid ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to {{f}}^{-1}\left[{x}\right]\subseteq \bigcup {J}$
9 cnvresima ${⊢}{\left({{f}↾}_{{y}}\right)}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]={{f}}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]\cap {y}$
10 4 ad2antrr ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {f}:\bigcup {J}⟶\bigcup {K}$
11 ffun ${⊢}{f}:\bigcup {J}⟶\bigcup {K}\to \mathrm{Fun}{f}$
12 inpreima ${⊢}\mathrm{Fun}{f}\to {{f}}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]={{f}}^{-1}\left[{x}\right]\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]$
13 10 11 12 3syl ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]={{f}}^{-1}\left[{x}\right]\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]$
14 13 ineq1d ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]\cap {y}=\left({{f}}^{-1}\left[{x}\right]\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]\right)\cap {y}$
15 in32 ${⊢}\left({{f}}^{-1}\left[{x}\right]\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]\right)\cap {y}=\left({{f}}^{-1}\left[{x}\right]\cap {y}\right)\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]$
16 ssrin ${⊢}{{f}}^{-1}\left[{x}\right]\subseteq \mathrm{dom}{f}\to {{f}}^{-1}\left[{x}\right]\cap {y}\subseteq \mathrm{dom}{f}\cap {y}$
17 5 16 ax-mp ${⊢}{{f}}^{-1}\left[{x}\right]\cap {y}\subseteq \mathrm{dom}{f}\cap {y}$
18 dminss ${⊢}\mathrm{dom}{f}\cap {y}\subseteq {{f}}^{-1}\left[{f}\left[{y}\right]\right]$
19 17 18 sstri ${⊢}{{f}}^{-1}\left[{x}\right]\cap {y}\subseteq {{f}}^{-1}\left[{f}\left[{y}\right]\right]$
20 19 a1i ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}}^{-1}\left[{x}\right]\cap {y}\subseteq {{f}}^{-1}\left[{f}\left[{y}\right]\right]$
21 df-ss ${⊢}{{f}}^{-1}\left[{x}\right]\cap {y}\subseteq {{f}}^{-1}\left[{f}\left[{y}\right]\right]↔\left({{f}}^{-1}\left[{x}\right]\cap {y}\right)\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]={{f}}^{-1}\left[{x}\right]\cap {y}$
22 20 21 sylib ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to \left({{f}}^{-1}\left[{x}\right]\cap {y}\right)\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]={{f}}^{-1}\left[{x}\right]\cap {y}$
23 15 22 syl5eq ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to \left({{f}}^{-1}\left[{x}\right]\cap {{f}}^{-1}\left[{f}\left[{y}\right]\right]\right)\cap {y}={{f}}^{-1}\left[{x}\right]\cap {y}$
24 14 23 eqtrd ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]\cap {y}={{f}}^{-1}\left[{x}\right]\cap {y}$
25 9 24 syl5eq ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {\left({{f}↾}_{{y}}\right)}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]={{f}}^{-1}\left[{x}\right]\cap {y}$
26 simpr ${⊢}\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\to {f}\in \left({J}\mathrm{Cn}{K}\right)$
27 26 ad2antrr ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {f}\in \left({J}\mathrm{Cn}{K}\right)$
28 elpwi ${⊢}{y}\in 𝒫\bigcup {J}\to {y}\subseteq \bigcup {J}$
29 28 ad2antrl ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {y}\subseteq \bigcup {J}$
30 1 cnrest ${⊢}\left({f}\in \left({J}\mathrm{Cn}{K}\right)\wedge {y}\subseteq \bigcup {J}\right)\to {{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}{K}\right)$
31 27 29 30 syl2anc ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}{K}\right)$
32 simpr ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {K}\in \mathrm{Top}$
33 32 ad3antrrr ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {K}\in \mathrm{Top}$
34 toptopon2 ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
35 33 34 sylib ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
36 df-ima ${⊢}{f}\left[{y}\right]=\mathrm{ran}\left({{f}↾}_{{y}}\right)$
37 36 eqimss2i ${⊢}\mathrm{ran}\left({{f}↾}_{{y}}\right)\subseteq {f}\left[{y}\right]$
38 37 a1i ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to \mathrm{ran}\left({{f}↾}_{{y}}\right)\subseteq {f}\left[{y}\right]$
39 imassrn ${⊢}{f}\left[{y}\right]\subseteq \mathrm{ran}{f}$
40 10 frnd ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to \mathrm{ran}{f}\subseteq \bigcup {K}$
41 39 40 sstrid ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {f}\left[{y}\right]\subseteq \bigcup {K}$
42 cnrest2 ${⊢}\left({K}\in \mathrm{TopOn}\left(\bigcup {K}\right)\wedge \mathrm{ran}\left({{f}↾}_{{y}}\right)\subseteq {f}\left[{y}\right]\wedge {f}\left[{y}\right]\subseteq \bigcup {K}\right)\to \left({{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}{K}\right)↔{{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)\right)\right)$
43 35 38 41 42 syl3anc ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to \left({{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}{K}\right)↔{{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)\right)\right)$
44 31 43 mpbid ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)\right)$
45 simplr ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {x}\in \mathrm{𝑘Gen}\left({K}\right)$
46 simprr ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {J}{↾}_{𝑡}{y}\in \mathrm{Comp}$
47 imacmp ${⊢}\left({f}\in \left({J}\mathrm{Cn}{K}\right)\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\to {K}{↾}_{𝑡}{f}\left[{y}\right]\in \mathrm{Comp}$
48 27 46 47 syl2anc ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {K}{↾}_{𝑡}{f}\left[{y}\right]\in \mathrm{Comp}$
49 kgeni ${⊢}\left({x}\in \mathrm{𝑘Gen}\left({K}\right)\wedge {K}{↾}_{𝑡}{f}\left[{y}\right]\in \mathrm{Comp}\right)\to {x}\cap {f}\left[{y}\right]\in \left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)$
50 45 48 49 syl2anc ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {x}\cap {f}\left[{y}\right]\in \left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)$
51 cnima ${⊢}\left({{f}↾}_{{y}}\in \left(\left({J}{↾}_{𝑡}{y}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)\right)\wedge {x}\cap {f}\left[{y}\right]\in \left({K}{↾}_{𝑡}{f}\left[{y}\right]\right)\right)\to {\left({{f}↾}_{{y}}\right)}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]\in \left({J}{↾}_{𝑡}{y}\right)$
52 44 50 51 syl2anc ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {\left({{f}↾}_{{y}}\right)}^{-1}\left[{x}\cap {f}\left[{y}\right]\right]\in \left({J}{↾}_{𝑡}{y}\right)$
53 25 52 eqeltrrd ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge \left({y}\in 𝒫\bigcup {J}\wedge {J}{↾}_{𝑡}{y}\in \mathrm{Comp}\right)\right)\to {{f}}^{-1}\left[{x}\right]\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)$
54 53 expr ${⊢}\left(\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\wedge {y}\in 𝒫\bigcup {J}\right)\to \left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {{f}}^{-1}\left[{x}\right]\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)$
55 54 ralrimiva ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {{f}}^{-1}\left[{x}\right]\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)$
56 kgentop ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to {J}\in \mathrm{Top}$
57 56 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to {J}\in \mathrm{Top}$
58 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
59 57 58 sylib ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
60 elkgen ${⊢}{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\to \left({{f}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\left({{f}}^{-1}\left[{x}\right]\subseteq \bigcup {J}\wedge \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {{f}}^{-1}\left[{x}\right]\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)\right)\right)$
61 59 60 syl ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to \left({{f}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\left({{f}}^{-1}\left[{x}\right]\subseteq \bigcup {J}\wedge \forall {y}\in 𝒫\bigcup {J}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{y}\in \mathrm{Comp}\to {{f}}^{-1}\left[{x}\right]\cap {y}\in \left({J}{↾}_{𝑡}{y}\right)\right)\right)\right)$
62 8 55 61 mpbir2and ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to {{f}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)$
63 kgenidm ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \mathrm{𝑘Gen}\left({J}\right)={J}$
64 63 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to \mathrm{𝑘Gen}\left({J}\right)={J}$
65 62 64 eleqtrd ${⊢}\left(\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\wedge {x}\in \mathrm{𝑘Gen}\left({K}\right)\right)\to {{f}}^{-1}\left[{x}\right]\in {J}$
66 65 ralrimiva ${⊢}\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\to \forall {x}\in \mathrm{𝑘Gen}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {J}$
67 56 58 sylib ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
68 kgentopon ${⊢}{K}\in \mathrm{TopOn}\left(\bigcup {K}\right)\to \mathrm{𝑘Gen}\left({K}\right)\in \mathrm{TopOn}\left(\bigcup {K}\right)$
69 34 68 sylbi ${⊢}{K}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left({K}\right)\in \mathrm{TopOn}\left(\bigcup {K}\right)$
70 iscn ${⊢}\left({J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\wedge \mathrm{𝑘Gen}\left({K}\right)\in \mathrm{TopOn}\left(\bigcup {K}\right)\right)\to \left({f}\in \left({J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)↔\left({f}:\bigcup {J}⟶\bigcup {K}\wedge \forall {x}\in \mathrm{𝑘Gen}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {J}\right)\right)$
71 67 69 70 syl2an ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to \left({f}\in \left({J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)↔\left({f}:\bigcup {J}⟶\bigcup {K}\wedge \forall {x}\in \mathrm{𝑘Gen}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {J}\right)\right)$
72 71 adantr ${⊢}\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\to \left({f}\in \left({J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)↔\left({f}:\bigcup {J}⟶\bigcup {K}\wedge \forall {x}\in \mathrm{𝑘Gen}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {J}\right)\right)$
73 4 66 72 mpbir2and ${⊢}\left(\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\wedge {f}\in \left({J}\mathrm{Cn}{K}\right)\right)\to {f}\in \left({J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)$
74 73 ex ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to \left({f}\in \left({J}\mathrm{Cn}{K}\right)\to {f}\in \left({J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)\right)$
75 74 ssrdv ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {J}\mathrm{Cn}{K}\subseteq {J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)$
76 69 adantl ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to \mathrm{𝑘Gen}\left({K}\right)\in \mathrm{TopOn}\left(\bigcup {K}\right)$
77 toponcom ${⊢}\left({K}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({K}\right)\in \mathrm{TopOn}\left(\bigcup {K}\right)\right)\to {K}\in \mathrm{TopOn}\left(\bigcup \mathrm{𝑘Gen}\left({K}\right)\right)$
78 32 76 77 syl2anc ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {K}\in \mathrm{TopOn}\left(\bigcup \mathrm{𝑘Gen}\left({K}\right)\right)$
79 kgenss ${⊢}{K}\in \mathrm{Top}\to {K}\subseteq \mathrm{𝑘Gen}\left({K}\right)$
80 79 adantl ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {K}\subseteq \mathrm{𝑘Gen}\left({K}\right)$
81 eqid ${⊢}\bigcup \mathrm{𝑘Gen}\left({K}\right)=\bigcup \mathrm{𝑘Gen}\left({K}\right)$
82 81 cnss2 ${⊢}\left({K}\in \mathrm{TopOn}\left(\bigcup \mathrm{𝑘Gen}\left({K}\right)\right)\wedge {K}\subseteq \mathrm{𝑘Gen}\left({K}\right)\right)\to {J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\subseteq {J}\mathrm{Cn}{K}$
83 78 80 82 syl2anc ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\subseteq {J}\mathrm{Cn}{K}$
84 75 83 eqssd ${⊢}\left({J}\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to {J}\mathrm{Cn}{K}={J}\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)$