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

Metamath Proof Explorer

Theorem hmeoqtop

Description: A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion hmeoqtop ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 = ( 𝐽 qTop 𝐹 ) )

Proof

Step Hyp Ref Expression
1 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
3 1 2 syl ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 ∈ Top )
4 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
5 3 4 sylib ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
8 6 7 hmeof1o ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 )
9 f1ofo ⊢ ( 𝐹 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 → 𝐹 : ∪ 𝐽 –onto→ ∪ 𝐾 )
10 forn ⊢ ( 𝐹 : ∪ 𝐽 –onto→ ∪ 𝐾 → ran 𝐹 = ∪ 𝐾 )
11 8 9 10 3syl ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ran 𝐹 = ∪ 𝐾 )
12 hmeoima ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
13 5 1 11 12 qtopomap ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 = ( 𝐽 qTop 𝐹 ) )