Theorem hmeocld

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	hmeoopn.1	$$⊢X=\bigcup J$$
Assertion	hmeocld	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(A\in \mathrm{Clsd}\left(J\right)\leftrightarrow F\left[A\right]\in \mathrm{Clsd}\left(K\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hmeoopn.1	$$⊢X=\bigcup J$$
2		hmeocnvcn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
3	2	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
4		imacnvcnv	$$⊢{F^{-1}}^{-1}\left[A\right]=F\left[A\right]$$
5		cnclima	$$⊢\left(F^{-1}\in \left(K\mathrm{Cn}J\right)\wedge A\in \mathrm{Clsd}\left(J\right)\right)\to {F^{-1}}^{-1}\left[A\right]\in \mathrm{Clsd}\left(K\right)$$
6	4 5	eqeltrrid	$$⊢\left(F^{-1}\in \left(K\mathrm{Cn}J\right)\wedge A\in \mathrm{Clsd}\left(J\right)\right)\to F\left[A\right]\in \mathrm{Clsd}\left(K\right)$$
7	6	ex	$$⊢F^{-1}\in \left(K\mathrm{Cn}J\right)\to \left(A\in \mathrm{Clsd}\left(J\right)\to F\left[A\right]\in \mathrm{Clsd}\left(K\right)\right)$$
8	3 7	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(A\in \mathrm{Clsd}\left(J\right)\to F\left[A\right]\in \mathrm{Clsd}\left(K\right)\right)$$
9		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
10	9	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F\in \left(J\mathrm{Cn}K\right)$$
11		cnclima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge F\left[A\right]\in \mathrm{Clsd}\left(K\right)\right)\to F^{-1}\left[F\left[A\right]\right]\in \mathrm{Clsd}\left(J\right)$$
12	11	ex	$$⊢F\in \left(J\mathrm{Cn}K\right)\to \left(F\left[A\right]\in \mathrm{Clsd}\left(K\right)\to F^{-1}\left[F\left[A\right]\right]\in \mathrm{Clsd}\left(J\right)\right)$$
13	10 12	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(F\left[A\right]\in \mathrm{Clsd}\left(K\right)\to F^{-1}\left[F\left[A\right]\right]\in \mathrm{Clsd}\left(J\right)\right)$$
14		eqid	$$⊢\bigcup K=\bigcup K$$
15	1 14	hmeof1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:X\underset{1-1\; onto}{⟶}\bigcup K$$
16		f1of1	$$⊢F:X\underset{1-1\; onto}{⟶}\bigcup K\to F:X\underset{1-1}{⟶}\bigcup K$$
17	15 16	syl	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:X\underset{1-1}{⟶}\bigcup K$$
18		f1imacnv	$$⊢\left(F:X\underset{1-1}{⟶}\bigcup K\wedge A\subseteq X\right)\to F^{-1}\left[F\left[A\right]\right]=A$$
19	17 18	sylan	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F^{-1}\left[F\left[A\right]\right]=A$$
20	19	eleq1d	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(F^{-1}\left[F\left[A\right]\right]\in \mathrm{Clsd}\left(J\right)\leftrightarrow A\in \mathrm{Clsd}\left(J\right)\right)$$
21	13 20	sylibd	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(F\left[A\right]\in \mathrm{Clsd}\left(K\right)\to A\in \mathrm{Clsd}\left(J\right)\right)$$
22	8 21	impbid	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(A\in \mathrm{Clsd}\left(J\right)\leftrightarrow F\left[A\right]\in \mathrm{Clsd}\left(K\right)\right)$$