Metamath Proof Explorer

Theorem hmeocls

Description: Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 hmeoopn.1 
 |-  X = U. J
2 hmeocnvcn 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
3 1 cncls2i 
 |-  ( ( `' F e. ( K Cn J ) /\ A C_ X ) -> ( ( cls ` K ) ` ( `' `' F " A ) ) C_ ( `' `' F " ( ( cls ` J ) ` A ) ) )
4 2 3 sylan 
 |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( cls ` K ) ` ( `' `' F " A ) ) C_ ( `' `' F " ( ( cls ` J ) ` A ) ) )
5 imacnvcnv 
 |-  ( `' `' F " A ) = ( F " A )
6 5 fveq2i 
 |-  ( ( cls ` K ) ` ( `' `' F " A ) ) = ( ( cls ` K ) ` ( F " A ) )
7 imacnvcnv 
 |-  ( `' `' F " ( ( cls ` J ) ` A ) ) = ( F " ( ( cls ` J ) ` A ) )
8 4 6 7 3sstr3g 
 |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( cls ` K ) ` ( F " A ) ) C_ ( F " ( ( cls ` J ) ` A ) ) )
9 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
10 1 cnclsi 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F " ( ( cls ` J ) ` A ) ) C_ ( ( cls ` K ) ` ( F " A ) ) )
11 9 10 sylan 
 |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( F " ( ( cls ` J ) ` A ) ) C_ ( ( cls ` K ) ` ( F " A ) ) )
12 8 11 eqssd 
 |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( cls ` K ) ` ( F " A ) ) = ( F " ( ( cls ` J ) ` A ) ) )