Metamath Proof Explorer

Theorem kgencn

Description: A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 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)$

Proof

Step Hyp Ref Expression
1 kgentopon ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left({X}\right)$
2 iscn ${⊢}\left(\mathrm{𝑘Gen}\left({J}\right)\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 {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)$
3 1 2 sylan ${⊢}\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 {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)$
4 cnvimass ${⊢}{{F}}^{-1}\left[{x}\right]\subseteq \mathrm{dom}{F}$
5 fdm ${⊢}{F}:{X}⟶{Y}\to \mathrm{dom}{F}={X}$
6 5 adantl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to \mathrm{dom}{F}={X}$
7 4 6 sseqtrid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to {{F}}^{-1}\left[{x}\right]\subseteq {X}$
8 elkgen ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\left({{F}}^{-1}\left[{x}\right]\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
9 8 ad2antrr ${⊢}\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({{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\left({{F}}^{-1}\left[{x}\right]\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
10 7 9 mpbirand ${⊢}\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({{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
11 10 ralbidv ${⊢}\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 {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
12 simpr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to {F}:{X}⟶{Y}$
13 elpwi ${⊢}{k}\in 𝒫{X}\to {k}\subseteq {X}$
14 fssres ${⊢}\left({F}:{X}⟶{Y}\wedge {k}\subseteq {X}\right)\to \left({{F}↾}_{{k}}\right):{k}⟶{Y}$
15 12 13 14 syl2an ${⊢}\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({{F}↾}_{{k}}\right):{k}⟶{Y}$
16 simpll ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
17 resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {k}\subseteq {X}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
18 16 13 17 syl2an ${⊢}\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 {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
19 simpllr ${⊢}\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}\in \mathrm{TopOn}\left({Y}\right)$
20 iscn ${⊢}\left({J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔\left(\left({{F}↾}_{{k}}\right):{k}⟶{Y}\wedge \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{{k}}\right)}^{-1}\left[{x}\right]\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
21 18 19 20 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({{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔\left(\left({{F}↾}_{{k}}\right):{k}⟶{Y}\wedge \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{{k}}\right)}^{-1}\left[{x}\right]\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
22 15 21 mpbirand ${⊢}\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({{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{{k}}\right)}^{-1}\left[{x}\right]\in \left({J}{↾}_{𝑡}{k}\right)\right)$
23 cnvresima ${⊢}{\left({{F}↾}_{{k}}\right)}^{-1}\left[{x}\right]={{F}}^{-1}\left[{x}\right]\cap {k}$
24 23 eleq1i ${⊢}{\left({{F}↾}_{{k}}\right)}^{-1}\left[{x}\right]\in \left({J}{↾}_{𝑡}{k}\right)↔{{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
25 24 ralbii ${⊢}\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{{k}}\right)}^{-1}\left[{x}\right]\in \left({J}{↾}_{𝑡}{k}\right)↔\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
26 22 25 syl6bb ${⊢}\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({{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)↔\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
27 26 imbi2d ${⊢}\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(\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)↔\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
28 r19.21v ${⊢}\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)↔\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
29 27 28 syl6bbr ${⊢}\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(\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}↾}_{{k}}\in \left(\left({J}{↾}_{𝑡}{k}\right)\mathrm{Cn}{K}\right)\right)↔\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
30 29 ralbidva ${⊢}\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 {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)$
31 ralcom ${⊢}\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)↔\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
32 30 31 syl6rbbr ${⊢}\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 {x}\in {K}\phantom{\rule{.4em}{0ex}}\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {{F}}^{-1}\left[{x}\right]\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)↔\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)$
33 11 32 bitrd ${⊢}\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 {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)↔\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)$
34 33 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 {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{𝑘Gen}\left({J}\right)\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)$
35 3 34 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 {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)$