Theorem hmeoqtop

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

	Ref	Expression
Assertion	hmeoqtop	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to K=J\mathrm{qTop}F$$

Proof

Step	Hyp	Ref	Expression
1		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
2		cntop2	$$⊢F\in \left(J\mathrm{Cn}K\right)\to K\in \mathrm{Top}$$
3	1 2	syl	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to K\in \mathrm{Top}$$
4		toptopon2	$$⊢K\in \mathrm{Top}\leftrightarrow K\in \mathrm{TopOn}\left(\bigcup K\right)$$
5	3 4	sylib	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to K\in \mathrm{TopOn}\left(\bigcup K\right)$$
6		eqid	$$⊢\bigcup J=\bigcup J$$
7		eqid	$$⊢\bigcup K=\bigcup K$$
8	6 7	hmeof1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:\bigcup J\underset{1-1\; onto}{⟶}\bigcup K$$
9		f1ofo	$$⊢F:\bigcup J\underset{1-1\; onto}{⟶}\bigcup K\to F:\bigcup J\underset{onto}{⟶}\bigcup K$$
10		forn	$$⊢F:\bigcup J\underset{onto}{⟶}\bigcup K\to \mathrm{ran}F=\bigcup K$$
11	8 9 10	3syl	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to \mathrm{ran}F=\bigcup K$$
12		hmeoima	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge x\in J\right)\to F\left[x\right]\in K$$
13	5 1 11 12	qtopomap	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to K=J\mathrm{qTop}F$$