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

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 ⊢ 𝑋 = ∪ 𝐽
hmeof1o.2 ⊢ 𝑌 = ∪ 𝐾
Assertion hmeof1o ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )

Proof

Step Hyp Ref Expression
1 hmeof1o.1 ⊢ 𝑋 = ∪ 𝐽
2 hmeof1o.2 ⊢ 𝑌 = ∪ 𝐾
3 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
5 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 4 5 sylib ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
8 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
9 7 8 sylib ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
10 6 9 jca ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) )
11 3 10 syl ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) )
12 hmeof1o2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
13 12 3expia ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
14 11 13 mpcom ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )