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	⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 “ 𝐴 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		hmeocnvcn	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
2		imacnvcnv	⊢ ( ◡ ◡ 𝐹 “ 𝐴 ) = ( 𝐹 “ 𝐴 )
3		cnima	⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝐴 ∈ 𝐽 ) → ( ◡ ◡ 𝐹 “ 𝐴 ) ∈ 𝐾 )
4	2 3	eqeltrrid	⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 “ 𝐴 ) ∈ 𝐾 )
5	1 4	sylan	⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 “ 𝐴 ) ∈ 𝐾 )