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 ) )