Description: A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | hmeoqtop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hmeocn | |
|
2 | cntop2 | |
|
3 | 1 2 | syl | |
4 | toptopon2 | |
|
5 | 3 4 | sylib | |
6 | eqid | |
|
7 | eqid | |
|
8 | 6 7 | hmeof1o | |
9 | f1ofo | |
|
10 | forn | |
|
11 | 8 9 10 | 3syl | |
12 | hmeoima | |
|
13 | 5 1 11 12 | qtopomap | |