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 𝐹 ) )