qtopcmap

Description: If F is a surjective continuous closed map, then it is a quotient map. (A closed map is a function that maps closed sets to closed 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$
	qtopcmap.7	$⊢ (φ \land x \in Clsd (J)) \to F [x] \in Clsd (K)$
Assertion	qtopcmap	$⊢ φ \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		qtopcmap.7	$⊢ (φ \land x \in Clsd (J)) \to F [x] \in Clsd (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		eqid	$⊢ ⋃ J = ⋃ J$
17	16	elqtop2	$⊢ (J \in Top \land F : ⋃ J \underset{onto}{⟶} Y) \to (y \in (J qTop F) \leftrightarrow (y \subseteq Y \land F^{-1} [y] \in J))$
18	8 15 17	syl2anc	$⊢ φ \to (y \in (J qTop F) \leftrightarrow (y \subseteq Y \land F^{-1} [y] \in J))$
19	15	adantr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F : ⋃ J \underset{onto}{⟶} Y$
20		difss	$⊢ Y ∖ y \subseteq Y$
21		foimacnv	$⊢ (F : ⋃ J \underset{onto}{⟶} Y \land Y ∖ y \subseteq Y) \to F [F^{-1} [Y ∖ y]] = Y ∖ y$
22	19 20 21	sylancl	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F [F^{-1} [Y ∖ y]] = Y ∖ y$
23	1	adantr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to K \in TopOn (Y)$
24		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
25	23 24	syl	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to Y = ⋃ K$
26	25	difeq1d	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to Y ∖ y = ⋃ K ∖ y$
27	22 26	eqtrd	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F [F^{-1} [Y ∖ y]] = ⋃ K ∖ y$
28		imaeq2	$⊢ x = F^{-1} [Y ∖ y] \to F [x] = F [F^{-1} [Y ∖ y]]$
29	28	eleq1d	$⊢ x = F^{-1} [Y ∖ y] \to (F [x] \in Clsd (K) \leftrightarrow F [F^{-1} [Y ∖ y]] \in Clsd (K))$
30	4	ralrimiva	$⊢ φ \to \forall x \in Clsd (J) F [x] \in Clsd (K)$
31	30	adantr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to \forall x \in Clsd (J) F [x] \in Clsd (K)$
32		fofun	$⊢ F : ⋃ J \underset{onto}{⟶} Y \to Fun F$
33		funcnvcnv	$⊢ Fun F \to Fun {F^{-1}}^{-1}$
34		imadif	$⊢ Fun {F^{-1}}^{-1} \to F^{-1} [Y ∖ y] = F^{-1} [Y] ∖ F^{-1} [y]$
35	19 32 33 34	4syl	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [Y ∖ y] = F^{-1} [Y] ∖ F^{-1} [y]$
36	12	adantr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F : ⋃ J ⟶ Y$
37		fimacnv	$⊢ F : ⋃ J ⟶ Y \to F^{-1} [Y] = ⋃ J$
38	36 37	syl	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [Y] = ⋃ J$
39	38	difeq1d	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [Y] ∖ F^{-1} [y] = ⋃ J ∖ F^{-1} [y]$
40	35 39	eqtrd	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [Y ∖ y] = ⋃ J ∖ F^{-1} [y]$
41	8	adantr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to J \in Top$
42		simprr	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [y] \in J$
43	16	opncld	$⊢ (J \in Top \land F^{-1} [y] \in J) \to ⋃ J ∖ F^{-1} [y] \in Clsd (J)$
44	41 42 43	syl2anc	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to ⋃ J ∖ F^{-1} [y] \in Clsd (J)$
45	40 44	eqeltrd	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F^{-1} [Y ∖ y] \in Clsd (J)$
46	29 31 45	rspcdva	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to F [F^{-1} [Y ∖ y]] \in Clsd (K)$
47	27 46	eqeltrrd	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to ⋃ K ∖ y \in Clsd (K)$
48		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
49	23 48	syl	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to K \in Top$
50		simprl	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to y \subseteq Y$
51	50 25	sseqtrd	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to y \subseteq ⋃ K$
52		eqid	$⊢ ⋃ K = ⋃ K$
53	52	isopn2	$⊢ (K \in Top \land y \subseteq ⋃ K) \to (y \in K \leftrightarrow ⋃ K ∖ y \in Clsd (K))$
54	49 51 53	syl2anc	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to (y \in K \leftrightarrow ⋃ K ∖ y \in Clsd (K))$
55	47 54	mpbird	$⊢ (φ \land (y \subseteq Y \land F^{-1} [y] \in J)) \to y \in K$
56	55	ex	$⊢ φ \to ((y \subseteq Y \land F^{-1} [y] \in J) \to y \in K)$
57	18 56	sylbid	$⊢ φ \to (y \in (J qTop F) \to y \in K)$
58	57	ssrdv	$⊢ φ \to J qTop F \subseteq K$
59	6 58	eqssd	$⊢ φ \to K = J qTop F$

Metamath Proof Explorer

Theorem qtopcmap

Proof