Metamath Proof Explorer

Theorem hmeocld

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis hmeoopn.1 
|- X = U. J
Assertion hmeocld 
|- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( F " A ) e. ( Clsd ` K ) ) )

Proof

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