hmeoqtop

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

		Ref	Expression
	Assertion	hmeoqtop	$⊢ F \in (J Homeo K) \to K = J qTop F$

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

Metamath Proof Explorer