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

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 ) )
4 3 adantr 
 |-  ( ( 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 ) )
9 8 adantr 
 |-  ( ( 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 ) )