# Metamath Proof Explorer

## 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 = U. J`
Assertion hmeoopn
`|- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. J <-> ( F " A ) e. K ) )`

### Proof

Step Hyp Ref Expression
1 hmeoopn.1
` |-  X = U. J`
2 hmeoima
` |-  ( ( F e. ( J Homeo K ) /\ A e. J ) -> ( F " A ) e. K )`
3 2 ex
` |-  ( F e. ( J Homeo K ) -> ( A e. J -> ( F " A ) e. K ) )`
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. J -> ( F " A ) e. K ) )`
5 hmeocn
` |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )`
6 cnima
` |-  ( ( F e. ( J Cn K ) /\ ( F " A ) e. K ) -> ( `' F " ( F " A ) ) e. J )`
7 6 ex
` |-  ( F e. ( J Cn K ) -> ( ( F " A ) e. K -> ( `' F " ( F " A ) ) e. J ) )`
8 5 7 syl
` |-  ( F e. ( J Homeo K ) -> ( ( F " A ) e. K -> ( `' F " ( F " A ) ) e. J ) )`
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( F " A ) e. K -> ( `' F " ( F " A ) ) e. J ) )`
10 eqid
` |-  U. K = U. K`
11 1 10 hmeof1o
` |-  ( F e. ( J Homeo K ) -> F : X -1-1-onto-> U. K )`
12 f1of1
` |-  ( F : X -1-1-onto-> U. K -> F : X -1-1-> U. K )`
13 11 12 syl
` |-  ( F e. ( J Homeo K ) -> F : X -1-1-> U. K )`
14 f1imacnv
` |-  ( ( F : X -1-1-> U. K /\ A C_ X ) -> ( `' F " ( F " A ) ) = A )`
15 13 14 sylan
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( `' F " ( F " A ) ) = A )`
16 15 eleq1d
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( `' F " ( F " A ) ) e. J <-> A e. J ) )`
17 9 16 sylibd
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( F " A ) e. K -> A e. J ) )`
18 4 17 impbid
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. J <-> ( F " A ) e. K ) )`