Metamath Proof Explorer

Theorem hmeoqtop

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

Ref Expression
Assertion hmeoqtop 
|- ( F e. ( J Homeo K ) -> K = ( J qTop F ) )

Proof

Step Hyp Ref Expression
1 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
2 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
3 1 2 syl 
 |-  ( F e. ( J Homeo K ) -> K e. Top )
4 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
5 3 4 sylib 
 |-  ( F e. ( J Homeo K ) -> K e. ( TopOn ` U. K ) )
6 eqid 
 |-  U. J = U. J
7 eqid 
 |-  U. K = U. K
8 6 7 hmeof1o 
 |-  ( F e. ( J Homeo K ) -> F : U. J -1-1-onto-> U. K )
9 f1ofo 
 |-  ( F : U. J -1-1-onto-> U. K -> F : U. J -onto-> U. K )
10 forn 
 |-  ( F : U. J -onto-> U. K -> ran F = U. K )
11 8 9 10 3syl 
 |-  ( F e. ( J Homeo K ) -> ran F = U. K )
12 hmeoima 
 |-  ( ( F e. ( J Homeo K ) /\ x e. J ) -> ( F " x ) e. K )
13 5 1 11 12 qtopomap 
 |-  ( F e. ( J Homeo K ) -> K = ( J qTop F ) )