Theorem cnclima

Description: A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	cnclima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to F^{-1}\left[A\right]\in \mathrm{Clsd}\left(J\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	adantr	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to F:\bigcup J⟶\bigcup K$$
5		ffun	$$⊢F:\bigcup J⟶\bigcup K\to \mathrm{Fun}F$$
6		funcnvcnv	$$⊢\mathrm{Fun}F\to \mathrm{Fun}{F^{-1}}^{-1}$$
7		imadif	$$⊢\mathrm{Fun}{F^{-1}}^{-1}\to F^{-1}\left[\bigcup K\setminus A\right]=F^{-1}\left[\bigcup K\right]\setminus F^{-1}\left[A\right]$$
8	5 6 7	3syl	$$⊢F:\bigcup J⟶\bigcup K\to F^{-1}\left[\bigcup K\setminus A\right]=F^{-1}\left[\bigcup K\right]\setminus F^{-1}\left[A\right]$$
9		fimacnv	$$⊢F:\bigcup J⟶\bigcup K\to F^{-1}\left[\bigcup K\right]=\bigcup J$$
10	9	difeq1d	$$⊢F:\bigcup J⟶\bigcup K\to F^{-1}\left[\bigcup K\right]\setminus F^{-1}\left[A\right]=\bigcup J\setminus F^{-1}\left[A\right]$$
11	8 10	eqtr2d	$$⊢F:\bigcup J⟶\bigcup K\to \bigcup J\setminus F^{-1}\left[A\right]=F^{-1}\left[\bigcup K\setminus A\right]$$
12	4 11	syl	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to \bigcup J\setminus F^{-1}\left[A\right]=F^{-1}\left[\bigcup K\setminus A\right]$$
13	2	cldopn	$$⊢A\in \mathrm{Clsd}\left(K\right)\to \bigcup K\setminus A\in K$$
14		cnima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge \bigcup K\setminus A\in K\right)\to F^{-1}\left[\bigcup K\setminus A\right]\in J$$
15	13 14	sylan2	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to F^{-1}\left[\bigcup K\setminus A\right]\in J$$
16	12 15	eqeltrd	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to \bigcup J\setminus F^{-1}\left[A\right]\in J$$
17		cntop1	$$⊢F\in \left(J\mathrm{Cn}K\right)\to J\in \mathrm{Top}$$
18		cnvimass	$$⊢F^{-1}\left[A\right]\subseteq \mathrm{dom}F$$
19	18 4	fssdm	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to F^{-1}\left[A\right]\subseteq \bigcup J$$
20	1	iscld2	$$⊢\left(J\in \mathrm{Top}\wedge F^{-1}\left[A\right]\subseteq \bigcup J\right)\to \left(F^{-1}\left[A\right]\in \mathrm{Clsd}\left(J\right)\leftrightarrow \bigcup J\setminus F^{-1}\left[A\right]\in J\right)$$
21	17 19 20	syl2an2r	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to \left(F^{-1}\left[A\right]\in \mathrm{Clsd}\left(J\right)\leftrightarrow \bigcup J\setminus F^{-1}\left[A\right]\in J\right)$$
22	16 21	mpbird	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge A\in \mathrm{Clsd}\left(K\right)\right)\to F^{-1}\left[A\right]\in \mathrm{Clsd}\left(J\right)$$