# Metamath Proof Explorer

## Theorem kgencn2

Description: A function F : J --> K from a compactly generated space is continuous iff for all compact spaces z and continuous g : z --> J , the composite F o. g : z --> K is continuous. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgencn2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left(\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 kgencn ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left(\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\right)\right)$
2 rncmp ${⊢}\left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\to {J}{↾}_{𝑡}\mathrm{ran}{g}\in \mathrm{Comp}$
3 2 adantl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to {J}{↾}_{𝑡}\mathrm{ran}{g}\in \mathrm{Comp}$
4 simprr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to {g}\in \left({z}\mathrm{Cn}{J}\right)$
5 eqid ${⊢}\bigcup {z}=\bigcup {z}$
6 eqid ${⊢}\bigcup {J}=\bigcup {J}$
7 5 6 cnf ${⊢}{g}\in \left({z}\mathrm{Cn}{J}\right)\to {g}:\bigcup {z}⟶\bigcup {J}$
8 frn ${⊢}{g}:\bigcup {z}⟶\bigcup {J}\to \mathrm{ran}{g}\subseteq \bigcup {J}$
9 4 7 8 3syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \mathrm{ran}{g}\subseteq \bigcup {J}$
10 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
11 10 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to {X}=\bigcup {J}$
12 9 11 sseqtrrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \mathrm{ran}{g}\subseteq {X}$
13 vex ${⊢}{g}\in \mathrm{V}$
14 13 rnex ${⊢}\mathrm{ran}{g}\in \mathrm{V}$
15 14 elpw ${⊢}\mathrm{ran}{g}\in 𝒫{X}↔\mathrm{ran}{g}\subseteq {X}$
16 12 15 sylibr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \mathrm{ran}{g}\in 𝒫{X}$
17 oveq2 ${⊢}{k}=\mathrm{ran}{g}\to {J}{↾}_{𝑡}{k}={J}{↾}_{𝑡}\mathrm{ran}{g}$
18 17 eleq1d ${⊢}{k}=\mathrm{ran}{g}\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}↔{J}{↾}_{𝑡}\mathrm{ran}{g}\in \mathrm{Comp}\right)$
19 reseq2 ${⊢}{k}=\mathrm{ran}{g}\to {{F}↾}_{{k}}={{F}↾}_{\mathrm{ran}{g}}$
20 17 oveq1d ${⊢}{k}=\mathrm{ran}{g}\to \left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}=\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}$
21 19 20 eleq12d ${⊢}{k}=\mathrm{ran}{g}\to \left({{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔{{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\right)$
22 18 21 imbi12d ${⊢}{k}=\mathrm{ran}{g}\to \left(\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)↔\left({J}{↾}_{𝑡}\mathrm{ran}{g}\in \mathrm{Comp}\to {{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\right)\right)$
23 22 rspcv ${⊢}\mathrm{ran}{g}\in 𝒫{X}\to \left(\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\to \left({J}{↾}_{𝑡}\mathrm{ran}{g}\in \mathrm{Comp}\to {{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\right)\right)$
24 16 23 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \left(\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\to \left({J}{↾}_{𝑡}\mathrm{ran}{g}\in \mathrm{Comp}\to {{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\right)\right)$
25 3 24 mpid ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \left(\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\to {{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\right)$
26 simplll ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
27 ssidd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \mathrm{ran}{g}\subseteq \mathrm{ran}{g}$
28 cnrest2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \mathrm{ran}{g}\subseteq \mathrm{ran}{g}\wedge \mathrm{ran}{g}\subseteq {X}\right)\to \left({g}\in \left({z}\mathrm{Cn}{J}\right)↔{g}\in \left({z}\mathrm{Cn}\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\right)\right)$
29 26 27 12 28 syl3anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \left({g}\in \left({z}\mathrm{Cn}{J}\right)↔{g}\in \left({z}\mathrm{Cn}\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\right)\right)$
30 4 29 mpbid ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to {g}\in \left({z}\mathrm{Cn}\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\right)$
31 cnco ${⊢}\left({g}\in \left({z}\mathrm{Cn}\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\right)\wedge {{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\right)\to \left({{F}↾}_{\mathrm{ran}{g}}\right)\circ {g}\in \left({z}\mathrm{Cn}{K}\right)$
32 31 ex ${⊢}{g}\in \left({z}\mathrm{Cn}\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\right)\to \left({{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\to \left({{F}↾}_{\mathrm{ran}{g}}\right)\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)$
33 30 32 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \left({{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\to \left({{F}↾}_{\mathrm{ran}{g}}\right)\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)$
34 ssid ${⊢}\mathrm{ran}{g}\subseteq \mathrm{ran}{g}$
35 cores ${⊢}\mathrm{ran}{g}\subseteq \mathrm{ran}{g}\to \left({{F}↾}_{\mathrm{ran}{g}}\right)\circ {g}={F}\circ {g}$
36 34 35 ax-mp ${⊢}\left({{F}↾}_{\mathrm{ran}{g}}\right)\circ {g}={F}\circ {g}$
37 36 eleq1i ${⊢}\left({{F}↾}_{\mathrm{ran}{g}}\right)\circ {g}\in \left({z}\mathrm{Cn}{K}\right)↔{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)$
38 33 37 syl6ib ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \left({{F}↾}_{\mathrm{ran}{g}}\in \left(\left({J}{↾}_{𝑡}\mathrm{ran}{g}\right)\mathrm{Cn}{K}\right)\to {F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)$
39 25 38 syld ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge \left({z}\in \mathrm{Comp}\wedge {g}\in \left({z}\mathrm{Cn}{J}\right)\right)\right)\to \left(\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\to {F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)$
40 39 ralrimdvva ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to \left(\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\to \forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)$
41 oveq1 ${⊢}{z}={J}{↾}_{𝑡}{k}\to {z}\mathrm{Cn}{J}=\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}$
42 oveq1 ${⊢}{z}={J}{↾}_{𝑡}{k}\to {z}\mathrm{Cn}{K}=\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}$
43 42 eleq2d ${⊢}{z}={J}{↾}_{𝑡}{k}\to \left({F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)↔{F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
44 41 43 raleqbidv ${⊢}{z}={J}{↾}_{𝑡}{k}\to \left(\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)↔\forall {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
45 44 rspcv ${⊢}{J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \left(\forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\to \forall {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
46 elpwi ${⊢}{k}\in 𝒫{X}\to {k}\subseteq {X}$
47 46 adantl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {k}\subseteq {X}$
48 47 resabs1d ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {\left({\mathrm{I}↾}_{{X}}\right)↾}_{{k}}={\mathrm{I}↾}_{{k}}$
49 idcn ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {\mathrm{I}↾}_{{X}}\in \left({J}\mathrm{Cn}{J}\right)$
50 49 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {\mathrm{I}↾}_{{X}}\in \left({J}\mathrm{Cn}{J}\right)$
51 10 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {X}=\bigcup {J}$
52 47 51 sseqtrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {k}\subseteq \bigcup {J}$
53 6 cnrest ${⊢}\left({\mathrm{I}↾}_{{X}}\in \left({J}\mathrm{Cn}{J}\right)\wedge {k}\subseteq \bigcup {J}\right)\to {\left({\mathrm{I}↾}_{{X}}\right)↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)$
54 50 52 53 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {\left({\mathrm{I}↾}_{{X}}\right)↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)$
55 48 54 eqeltrrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to {\mathrm{I}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)$
56 coeq2 ${⊢}{g}={\mathrm{I}↾}_{{k}}\to {F}\circ {g}={F}\circ \left({\mathrm{I}↾}_{{k}}\right)$
57 56 eleq1d ${⊢}{g}={\mathrm{I}↾}_{{k}}\to \left({F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔{F}\circ \left({\mathrm{I}↾}_{{k}}\right)\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
58 57 rspcv ${⊢}{\mathrm{I}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)\to \left(\forall {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\to {F}\circ \left({\mathrm{I}↾}_{{k}}\right)\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
59 55 58 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to \left(\forall {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\to {F}\circ \left({\mathrm{I}↾}_{{k}}\right)\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
60 coires1 ${⊢}{F}\circ \left({\mathrm{I}↾}_{{k}}\right)={{F}↾}_{{k}}$
61 60 eleq1i ${⊢}{F}\circ \left({\mathrm{I}↾}_{{k}}\right)\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔{{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)$
62 59 61 syl6ib ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to \left(\forall {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)$
63 45 62 syl9r ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \left(\forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\right)$
64 63 com23 ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\wedge {k}\in 𝒫{X}\right)\to \left(\forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\right)$
65 64 ralrimdva ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to \left(\forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\to \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\right)$
66 40 65 impbid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to \left(\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)↔\forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)$
67 66 pm5.32da ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left(\left({F}:{X}⟶{Y}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)\right)↔\left({F}:{X}⟶{Y}\wedge \forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)\right)$
68 1 67 bitrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left(\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {z}\in \mathrm{Comp}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({z}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}{F}\circ {g}\in \left({z}\mathrm{Cn}{K}\right)\right)\right)$