Metamath Proof Explorer


Theorem hmeoqtop

Description: A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion hmeoqtop FJHomeoKK=JqTopF

Proof

Step Hyp Ref Expression
1 hmeocn FJHomeoKFJCnK
2 cntop2 FJCnKKTop
3 1 2 syl FJHomeoKKTop
4 toptopon2 KTopKTopOnK
5 3 4 sylib FJHomeoKKTopOnK
6 eqid J=J
7 eqid K=K
8 6 7 hmeof1o FJHomeoKF:J1-1 ontoK
9 f1ofo F:J1-1 ontoKF:JontoK
10 forn F:JontoKranF=K
11 8 9 10 3syl FJHomeoKranF=K
12 hmeoima FJHomeoKxJFxK
13 5 1 11 12 qtopomap FJHomeoKK=JqTopF