# Metamath Proof Explorer

## Theorem cncls2

Description: Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cncls2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {x}\in 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\right)$

### Proof

Step Hyp Ref Expression
1 cnf2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\wedge {F}\in \left({J}\mathrm{Cn}{K}\right)\right)\to {F}:{X}⟶{Y}$
2 1 3expia ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}:{X}⟶{Y}\right)$
3 elpwi ${⊢}{x}\in 𝒫{Y}\to {x}\subseteq {Y}$
4 3 adantl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in 𝒫{Y}\right)\to {x}\subseteq {Y}$
5 toponuni ${⊢}{K}\in \mathrm{TopOn}\left({Y}\right)\to {Y}=\bigcup {K}$
6 5 ad2antlr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in 𝒫{Y}\right)\to {Y}=\bigcup {K}$
7 4 6 sseqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in 𝒫{Y}\right)\to {x}\subseteq \bigcup {K}$
8 eqid ${⊢}\bigcup {K}=\bigcup {K}$
9 8 cncls2i ${⊢}\left({F}\in \left({J}\mathrm{Cn}{K}\right)\wedge {x}\subseteq \bigcup {K}\right)\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]$
10 9 expcom ${⊢}{x}\subseteq \bigcup {K}\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)$
11 7 10 syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in 𝒫{Y}\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)$
12 11 ralrimdva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)\to \forall {x}\in 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)$
13 2 12 jcad ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)\to \left({F}:{X}⟶{Y}\wedge \forall {x}\in 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\right)$
14 8 cldss2 ${⊢}\mathrm{Clsd}\left({K}\right)\subseteq 𝒫\bigcup {K}$
15 5 ad2antlr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to {Y}=\bigcup {K}$
16 15 pweqd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {F}:{X}⟶{Y}\right)\to 𝒫{Y}=𝒫\bigcup {K}$
17 14 16 sseqtrrid ${⊢}\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{Clsd}\left({K}\right)\subseteq 𝒫{Y}$
18 17 sseld ${⊢}\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({x}\in \mathrm{Clsd}\left({K}\right)\to {x}\in 𝒫{Y}\right)$
19 18 imim1d ${⊢}\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(\left({x}\in 𝒫{Y}\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\to \left({x}\in \mathrm{Clsd}\left({K}\right)\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\right)$
20 cldcls ${⊢}{x}\in \mathrm{Clsd}\left({K}\right)\to \mathrm{cls}\left({K}\right)\left({x}\right)={x}$
21 20 ad2antll ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to \mathrm{cls}\left({K}\right)\left({x}\right)={x}$
22 21 imaeq2d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]={{F}}^{-1}\left[{x}\right]$
23 22 sseq2d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to \left(\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]↔\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[{x}\right]\right)$
24 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
25 24 ad2antrr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to {J}\in \mathrm{Top}$
26 cnvimass ${⊢}{{F}}^{-1}\left[{x}\right]\subseteq \mathrm{dom}{F}$
27 fdm ${⊢}{F}:{X}⟶{Y}\to \mathrm{dom}{F}={X}$
28 27 ad2antrl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to \mathrm{dom}{F}={X}$
29 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
30 29 ad2antrr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to {X}=\bigcup {J}$
31 28 30 eqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to \mathrm{dom}{F}=\bigcup {J}$
32 26 31 sseqtrid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to {{F}}^{-1}\left[{x}\right]\subseteq \bigcup {J}$
33 eqid ${⊢}\bigcup {J}=\bigcup {J}$
34 33 iscld4 ${⊢}\left({J}\in \mathrm{Top}\wedge {{F}}^{-1}\left[{x}\right]\subseteq \bigcup {J}\right)\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[{x}\right]\right)$
35 25 32 34 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[{x}\right]\right)$
36 23 35 bitr4d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({F}:{X}⟶{Y}\wedge {x}\in \mathrm{Clsd}\left({K}\right)\right)\right)\to \left(\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]↔{{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)$
37 36 expr ${⊢}\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({x}\in \mathrm{Clsd}\left({K}\right)\to \left(\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]↔{{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$
38 37 pm5.74d ${⊢}\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(\left({x}\in \mathrm{Clsd}\left({K}\right)\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)↔\left({x}\in \mathrm{Clsd}\left({K}\right)\to {{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$
39 19 38 sylibd ${⊢}\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(\left({x}\in 𝒫{Y}\to \mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\to \left({x}\in \mathrm{Clsd}\left({K}\right)\to {{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$
40 39 ralimdv2 ${⊢}\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 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\to \forall {x}\in \mathrm{Clsd}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)$
41 40 imdistanda ${⊢}\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 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\to \left({F}:{X}⟶{Y}\wedge \forall {x}\in \mathrm{Clsd}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$
42 iscncl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {x}\in \mathrm{Clsd}\left({K}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$
43 41 42 sylibrd ${⊢}\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 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\to {F}\in \left({J}\mathrm{Cn}{K}\right)\right)$
44 13 43 impbid ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {x}\in 𝒫{Y}\phantom{\rule{.4em}{0ex}}\mathrm{cls}\left({J}\right)\left({{F}}^{-1}\left[{x}\right]\right)\subseteq {{F}}^{-1}\left[\mathrm{cls}\left({K}\right)\left({x}\right)\right]\right)\right)$