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

Metamath Proof Explorer

Theorem hmeof1o2

Description: A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion hmeof1o2 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F : X -1-1-onto-> Y )

Proof

Step Hyp Ref Expression
1 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
2 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : X --> Y )
3 1 2 syl3an3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F : X --> Y )
4 3 ffnd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F Fn X )
5 hmeocnvcn 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
6 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ J e. ( TopOn ` X ) /\ `' F e. ( K Cn J ) ) -> `' F : Y --> X )
7 6 3com12 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ `' F e. ( K Cn J ) ) -> `' F : Y --> X )
8 5 7 syl3an3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> `' F : Y --> X )
9 8 ffnd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> `' F Fn Y )
10 dff1o4 
 |-  ( F : X -1-1-onto-> Y <-> ( F Fn X /\ `' F Fn Y ) )
11 4 9 10 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F : X -1-1-onto-> Y )