qtopomap

Description: If F is a surjective continuous open map, then it is a quotient map. (An open map is a function that maps open sets to open sets.) (Contributed by Mario Carneiro, 24-Mar-2015)

	Ref	Expression
Hypotheses	qtopomap.4	$⊢ φ \to K \in TopOn (Y)$
	qtopomap.5	$⊢ φ \to F \in (J Cn K)$
	qtopomap.6	$⊢ φ \to ran F = Y$
	qtopomap.7	$⊢ (φ \land x \in J) \to F [x] \in K$
Assertion	qtopomap	$⊢ φ \to K = J qTop F$

Proof

Step	Hyp	Ref	Expression
1		qtopomap.4	$⊢ φ \to K \in TopOn (Y)$
2		qtopomap.5	$⊢ φ \to F \in (J Cn K)$
3		qtopomap.6	$⊢ φ \to ran F = Y$
4		qtopomap.7	$⊢ (φ \land x \in J) \to F [x] \in K$
5		qtopss	$⊢ (F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \to K \subseteq J qTop F$
6	2 1 3 5	syl3anc	$⊢ φ \to K \subseteq J qTop F$
7		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
8	2 7	syl	$⊢ φ \to J \in Top$
9		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
10	8 9	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
11		cnf2	$⊢ (J \in TopOn (⋃ J) \land K \in TopOn (Y) \land F \in (J Cn K)) \to F : ⋃ J ⟶ Y$
12	10 1 2 11	syl3anc	$⊢ φ \to F : ⋃ J ⟶ Y$
13	12	ffnd	$⊢ φ \to F Fn ⋃ J$
14		df-fo	$⊢ F : ⋃ J \underset{onto}{⟶} Y \leftrightarrow (F Fn ⋃ J \land ran F = Y)$
15	13 3 14	sylanbrc	$⊢ φ \to F : ⋃ J \underset{onto}{⟶} Y$
16		elqtop3	$⊢ (J \in TopOn (⋃ J) \land F : ⋃ J \underset{onto}{⟶} Y) \to (y \in (J qTop F) \leftrightarrow (y \subseteq Y \land F^{-1} [y] \in J))$
17	10 15 16	syl2anc	$⊢ φ \to (y \in (J qTop F) \leftrightarrow (y \subseteq Y \land F^{-1} [y] \in J))$
18		foimacnv	$⊢ (F : ⋃ J \underset{onto}{⟶} Y \land y \subseteq Y) \to F [F^{-1} [y]] = y$
19	15 18	sylan	$⊢ (φ \land y \subseteq Y) \to F [F^{-1} [y]] = y$
20	19	adantrr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F [F^{-1} [y]] = y$
21		imaeq2	$⊢ x = F^{-1} [y] \to F [x] = F [F^{-1} [y]]$
22	21	eleq1d	$⊢ x = F^{-1} [y] \to (F [x] \in K \leftrightarrow F [F^{-1} [y]] \in K)$
23	4	ralrimiva	$⊢ φ \to \forall x \in J F [x] \in K$
24	23	adantr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to \forall x \in J F [x] \in K$
25		simprr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [y] \in J$
26	22 24 25	rspcdva	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F [F^{-1} [y]] \in K$
27	20 26	eqeltrrd	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to y \in K$
28	27	ex	$⊢ φ \to ((y \subseteq Y \land F^{-1} [y] \in J) \to y \in K)$
29	17 28	sylbid	$⊢ φ \to (y \in (J qTop F) \to y \in K)$
30	29	ssrdv	$⊢ φ \to J qTop F \subseteq K$
31	6 30	eqssd	$⊢ φ \to K = J qTop F$

Metamath Proof Explorer

Theorem qtopomap

Proof