This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ ( 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→ 𝑌 )