Step |
Hyp |
Ref |
Expression |
1 |
|
hmeocnvcn |
|- ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) ) |
2 |
1
|
3ad2ant3 |
|- ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) -> `' F e. ( K Cn J ) ) |
3 |
|
imacnvcnv |
|- ( `' `' F " S ) = ( F " S ) |
4 |
|
cnclima |
|- ( ( `' F e. ( K Cn J ) /\ S e. ( Clsd ` J ) ) -> ( `' `' F " S ) e. ( Clsd ` K ) ) |
5 |
3 4
|
eqeltrrid |
|- ( ( `' F e. ( K Cn J ) /\ S e. ( Clsd ` J ) ) -> ( F " S ) e. ( Clsd ` K ) ) |
6 |
2 5
|
sylan |
|- ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` J ) ) -> ( F " S ) e. ( Clsd ` K ) ) |