# 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 )`