hmeof1o2

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

		Ref	Expression
	Assertion	hmeof1o2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F : X \underset{1-1 onto}{⟶} Y$

Step	Hyp	Ref	Expression
1		hmeocn	$⊢ F \in (J Homeo K) \to F \in (J Cn K)$
2		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Cn K)) \to F : X ⟶ Y$
3	1 2	syl3an3	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F : X ⟶ Y$
4	3	ffnd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F Fn X$
5		hmeocnvcn	$⊢ F \in (J Homeo K) \to F^{-1} \in (K Cn J)$
6		cnf2	$⊢ (K \in TopOn (Y) \land J \in TopOn (X) \land F^{-1} \in (K Cn J)) \to F^{-1} : Y ⟶ X$
7	6	3com12	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F^{-1} \in (K Cn J)) \to F^{-1} : Y ⟶ X$
8	5 7	syl3an3	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F^{-1} : Y ⟶ X$
9	8	ffnd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F^{-1} Fn Y$
10		dff1o4	$⊢ F : X \underset{1-1 onto}{⟶} Y \leftrightarrow (F Fn X \land F^{-1} Fn Y)$
11	4 9 10	sylanbrc	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F : X \underset{1-1 onto}{⟶} Y$

Metamath Proof Explorer