Theorem hmeoima

Description: The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	hmeoima	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\in J\right)\to F\left[A\right]\in K$$

Proof

Step	Hyp	Ref	Expression
1		hmeocnvcn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
2		imacnvcnv	$$⊢{F^{-1}}^{-1}\left[A\right]=F\left[A\right]$$
3		cnima	$$⊢\left(F^{-1}\in \left(K\mathrm{Cn}J\right)\wedge A\in J\right)\to {F^{-1}}^{-1}\left[A\right]\in K$$
4	2 3	eqeltrrid	$$⊢\left(F^{-1}\in \left(K\mathrm{Cn}J\right)\wedge A\in J\right)\to F\left[A\right]\in K$$
5	1 4	sylan	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\in J\right)\to F\left[A\right]\in K$$