Description: Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hmeoopn.1 | |
|
Assertion | hmeocls | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hmeoopn.1 | |
|
2 | hmeocnvcn | |
|
3 | 1 | cncls2i | |
4 | 2 3 | sylan | |
5 | imacnvcnv | |
|
6 | 5 | fveq2i | |
7 | imacnvcnv | |
|
8 | 4 6 7 | 3sstr3g | |
9 | hmeocn | |
|
10 | 1 | cnclsi | |
11 | 9 10 | sylan | |
12 | 8 11 | eqssd | |