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 e. ( J Homeo K ) /\ A e. J ) -> ( F " A ) e. K )

Proof

Step Hyp Ref Expression
1 hmeocnvcn 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
2 imacnvcnv 
 |-  ( `' `' F " A ) = ( F " A )
3 cnima 
 |-  ( ( `' F e. ( K Cn J ) /\ A e. J ) -> ( `' `' F " A ) e. K )
4 2 3 eqeltrrid 
 |-  ( ( `' F e. ( K Cn J ) /\ A e. J ) -> ( F " A ) e. K )
5 1 4 sylan 
 |-  ( ( F e. ( J Homeo K ) /\ A e. J ) -> ( F " A ) e. K )