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 ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F : X ⟶ 1-1 onto Y

Proof

Step Hyp Ref Expression
1 hmeocn ⊢ F ∈ J Homeo K → F ∈ J Cn K
2 cnf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Cn K → F : X ⟶ Y
3 1 2 syl3an3 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F : X ⟶ Y
4 3 ffnd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F Fn X
5 hmeocnvcn ⊢ F ∈ J Homeo K → F -1 ∈ K Cn J
6 cnf2 ⊢ K ∈ TopOn ⁡ Y ∧ J ∈ TopOn ⁡ X ∧ F -1 ∈ K Cn J → F -1 : Y ⟶ X
7 6 3com12 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F -1 ∈ K Cn J → F -1 : Y ⟶ X
8 5 7 syl3an3 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F -1 : Y ⟶ X
9 8 ffnd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F -1 Fn Y
10 dff1o4 ⊢ F : X ⟶ 1-1 onto Y ↔ F Fn X ∧ F -1 Fn Y
11 4 9 10 sylanbrc ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F : X ⟶ 1-1 onto Y