This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (F \in (J Homeo K) \land A \in J) \to F [A] \in K$

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