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 = ⋃ J
hmeof1o.2 ⊢ Y = ⋃ K
Assertion hmeof1o ⊢ F ∈ J Homeo K → F : X ⟶ 1-1 onto Y

Proof

Step Hyp Ref Expression
1 hmeof1o.1 ⊢ X = ⋃ J
2 hmeof1o.2 ⊢ Y = ⋃ K
3 hmeocn ⊢ F ∈ J Homeo K → F ∈ J Cn K
4 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
5 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
6 4 5 sylib ⊢ F ∈ J Cn K → J ∈ TopOn ⁡ X
7 cntop2 ⊢ F ∈ J Cn K → K ∈ Top
8 2 toptopon ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ Y
9 7 8 sylib ⊢ F ∈ J Cn K → K ∈ TopOn ⁡ Y
10 6 9 jca ⊢ F ∈ J Cn K → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y
11 3 10 syl ⊢ F ∈ J Homeo K → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y
12 hmeof1o2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Homeo K → F : X ⟶ 1-1 onto Y
13 12 3expia ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Homeo K → F : X ⟶ 1-1 onto Y
14 11 13 mpcom ⊢ F ∈ J Homeo K → F : X ⟶ 1-1 onto Y