Description: Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | hmeocldb | |- ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` K ) ) -> ( `' F " S ) e. ( Clsd ` J ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hmeocn | |- ( F e. ( J Homeo K ) -> F e. ( J Cn K ) ) |
|
2 | 1 | 3ad2ant3 | |- ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) -> F e. ( J Cn K ) ) |
3 | cnclima | |- ( ( F e. ( J Cn K ) /\ S e. ( Clsd ` K ) ) -> ( `' F " S ) e. ( Clsd ` J ) ) |
|
4 | 2 3 | sylan | |- ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` K ) ) -> ( `' F " S ) e. ( Clsd ` J ) ) |