Theorem 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	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	qtopomap.5	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	qtopomap.6	⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
	qtopcmap.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
Assertion	qtopcmap	⊢ ( 𝜑 → 𝐾 = ( 𝐽 qTop 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		qtopomap.4	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
2		qtopomap.5	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		qtopomap.6	⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
4		qtopcmap.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
5		qtopss	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) )
6	2 1 3 5	syl3anc	⊢ ( 𝜑 → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) )
7		cntop1	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
8	2 7	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
9		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
10	8 9	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
12	10 1 2 11	syl3anc	⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
13	12	ffnd	⊢ ( 𝜑 → 𝐹 Fn ∪ 𝐽 )
14		df-fo	⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ↔ ( 𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌 ) )
15	13 3 14	sylanbrc	⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
16		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
17	16	elqtop2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
18	8 15 17	syl2anc	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
19	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
20		difss	⊢ ( 𝑌 ∖ 𝑦 ) ⊆ 𝑌
21		foimacnv	⊢ ( ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ∧ ( 𝑌 ∖ 𝑦 ) ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) = ( 𝑌 ∖ 𝑦 ) )
22	19 20 21	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) = ( 𝑌 ∖ 𝑦 ) )
23	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
24		toponuni	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
25	23 24	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑌 = ∪ 𝐾 )
26	25	difeq1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑌 ∖ 𝑦 ) = ( ∪ 𝐾 ∖ 𝑦 ) )
27	22 26	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) = ( ∪ 𝐾 ∖ 𝑦 ) )
28		imaeq2	⊢ ( 𝑥 = ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) )
29	28	eleq1d	⊢ ( 𝑥 = ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) → ( ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ↔ ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) ∈ ( Clsd ‘ 𝐾 ) ) )
30	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
32		fofun	⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 → Fun 𝐹 )
33		funcnvcnv	⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
34		imadif	⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
35	19 32 33 34	4syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
36	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
37		fimacnv	⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
38	36 37	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
39	38	difeq1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝑦 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
40	35 39	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
41	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐽 ∈ Top )
42		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
43	16	opncld	⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
44	41 42 43	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
45	40 44	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
46	29 31 45	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) ∈ ( Clsd ‘ 𝐾 ) )
47	27 46	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ∪ 𝐾 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐾 ) )
48		topontop	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
49	23 48	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐾 ∈ Top )
50		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ⊆ 𝑌 )
51	50 25	sseqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ⊆ ∪ 𝐾 )
52		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
53	52	isopn2	⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾 ) → ( 𝑦 ∈ 𝐾 ↔ ( ∪ 𝐾 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐾 ) ) )
54	49 51 53	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑦 ∈ 𝐾 ↔ ( ∪ 𝐾 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐾 ) ) )
55	47 54	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ∈ 𝐾 )
56	55	ex	⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → 𝑦 ∈ 𝐾 ) )
57	18 56	sylbid	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) → 𝑦 ∈ 𝐾 ) )
58	57	ssrdv	⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ⊆ 𝐾 )
59	6 58	eqssd	⊢ ( 𝜑 → 𝐾 = ( 𝐽 qTop 𝐹 ) )