This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hmeof1o

Description: A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses hmeof1o.1 
|- X = U. J
hmeof1o.2 
|- Y = U. K
Assertion hmeof1o 
|- ( F e. ( J Homeo K ) -> F : X -1-1-onto-> Y )

Proof

Step Hyp Ref Expression
1 hmeof1o.1 
 |-  X = U. J
2 hmeof1o.2 
 |-  Y = U. K
3 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
4 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
5 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
6 4 5 sylib 
 |-  ( F e. ( J Cn K ) -> J e. ( TopOn ` X ) )
7 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
8 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
9 7 8 sylib 
 |-  ( F e. ( J Cn K ) -> K e. ( TopOn ` Y ) )
10 6 9 jca 
 |-  ( F e. ( J Cn K ) -> ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) )
11 3 10 syl 
 |-  ( F e. ( J Homeo K ) -> ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) )
12 hmeof1o2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F : X -1-1-onto-> Y )
13 12 3expia 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Homeo K ) -> F : X -1-1-onto-> Y ) )
14 11 13 mpcom 
 |-  ( F e. ( J Homeo K ) -> F : X -1-1-onto-> Y )