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 )