Theorem hmeoopn

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

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

Proof

Step	Hyp	Ref	Expression
1		hmeoopn.1	$$⊢X=\bigcup J$$
2		hmeoima	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\in J\right)\to F\left[A\right]\in K$$
3	2	ex	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to \left(A\in J\to F\left[A\right]\in K\right)$$
4	3	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(A\in J\to F\left[A\right]\in K\right)$$
5		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
6		cnima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge F\left[A\right]\in K\right)\to F^{-1}\left[F\left[A\right]\right]\in J$$
7	6	ex	$$⊢F\in \left(J\mathrm{Cn}K\right)\to \left(F\left[A\right]\in K\to F^{-1}\left[F\left[A\right]\right]\in J\right)$$
8	5 7	syl	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to \left(F\left[A\right]\in K\to F^{-1}\left[F\left[A\right]\right]\in J\right)$$
9	8	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(F\left[A\right]\in K\to F^{-1}\left[F\left[A\right]\right]\in J\right)$$
10		eqid	$$⊢\bigcup K=\bigcup K$$
11	1 10	hmeof1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:X\underset{1-1\; onto}{⟶}\bigcup K$$
12		f1of1	$$⊢F:X\underset{1-1\; onto}{⟶}\bigcup K\to F:X\underset{1-1}{⟶}\bigcup K$$
13	11 12	syl	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:X\underset{1-1}{⟶}\bigcup K$$
14		f1imacnv	$$⊢\left(F:X\underset{1-1}{⟶}\bigcup K\wedge A\subseteq X\right)\to F^{-1}\left[F\left[A\right]\right]=A$$
15	13 14	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$$
16	15	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 J\leftrightarrow A\in J\right)$$
17	9 16	sylibd	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(F\left[A\right]\in K\to A\in J\right)$$
18	4 17	impbid	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(A\in J\leftrightarrow F\left[A\right]\in K\right)$$