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