Theorem hmeof1o2

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

	Ref	Expression
Assertion	hmeof1o2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		hmeocn	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
3	1 2	syl3an3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
4	3	ffnd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐹 Fn 𝑋 )
5		hmeocnvcn	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
6		cnf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
7	6	3com12	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
8	5 7	syl3an3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
9	8	ffnd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → ◡ 𝐹 Fn 𝑌 )
10		dff1o4	⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ( 𝐹 Fn 𝑋 ∧ ◡ 𝐹 Fn 𝑌 ) )
11	4 9 10	sylanbrc	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )