Theorem qtopcmap 21893

Description: If 𝐹 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.)

Hypotheses

Ref	Expression
qtopomap.4	⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
qtopomap.5	⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
qtopomap.6	⊢ (𝜑 → ran 𝐹 = 𝑌)
qtopcmap.7	⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾))

Assertion

Ref	Expression
qtopcmap	⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹))

Distinct variable groups:   𝑥,𝐹   𝑥,𝐽   𝑥,𝐾   𝜑,𝑥   𝑥,𝑌

Proof of Theorem qtopcmap

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		qtopomap.5	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
2		qtopomap.4	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
3		qtopomap.6	. . 3 ⊢ (𝜑 → ran 𝐹 = 𝑌)
4		qtopss 21889	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 = 𝑌) → 𝐾 ⊆ (𝐽 qTop 𝐹))
5	1, 2, 3, 4	syl3anc 1494	. 2 ⊢ (𝜑 → 𝐾 ⊆ (𝐽 qTop 𝐹))
6		cntop1 21415	. . . . . 6 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
7	1, 6	syl 17	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ Top)
8		eqid 2825	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
9	8	toptopon 21092	. . . . . . . . 9 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
10	7, 9	sylib 210	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
11		cnf2 21424	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶𝑌)
12	10, 2, 1, 11	syl3anc 1494	. . . . . . 7 ⊢ (𝜑 → 𝐹:∪ 𝐽⟶𝑌)
13	12	ffnd 6279	. . . . . 6 ⊢ (𝜑 → 𝐹 Fn ∪ 𝐽)
14		df-fo 6129	. . . . . 6 ⊢ (𝐹:∪ 𝐽–onto→𝑌 ↔ (𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌))
15	13, 3, 14	sylanbrc 578	. . . . 5 ⊢ (𝜑 → 𝐹:∪ 𝐽–onto→𝑌)
16	8	elqtop2 21875	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐹:∪ 𝐽–onto→𝑌) → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)))
17	7, 15, 16	syl2anc 579	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)))
18	15	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐹:∪ 𝐽–onto→𝑌)
19		difss 3964	. . . . . . . . 9 ⊢ (𝑌 ∖ 𝑦) ⊆ 𝑌
20		foimacnv 6395	. . . . . . . . 9 ⊢ ((𝐹:∪ 𝐽–onto→𝑌 ∧ (𝑌 ∖ 𝑦) ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) = (𝑌 ∖ 𝑦))
21	18, 19, 20	sylancl 580	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) = (𝑌 ∖ 𝑦))
22	2	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐾 ∈ (TopOn‘𝑌))
23		toponuni 21089	. . . . . . . . . 10 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
24	22, 23	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑌 = ∪ 𝐾)
25	24	difeq1d 3954	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝑌 ∖ 𝑦) = (∪ 𝐾 ∖ 𝑦))
26	21, 25	eqtrd 2861	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) = (∪ 𝐾 ∖ 𝑦))
27		imaeq2 5703	. . . . . . . . 9 ⊢ (𝑥 = (◡𝐹 “ (𝑌 ∖ 𝑦)) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))))
28	27	eleq1d 2891	. . . . . . . 8 ⊢ (𝑥 = (◡𝐹 “ (𝑌 ∖ 𝑦)) → ((𝐹 “ 𝑥) ∈ (Clsd‘𝐾) ↔ (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) ∈ (Clsd‘𝐾)))
29		qtopcmap.7	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾))
30	29	ralrimiva 3175	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (Clsd‘𝐽)(𝐹 “ 𝑥) ∈ (Clsd‘𝐾))
31	30	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∀𝑥 ∈ (Clsd‘𝐽)(𝐹 “ 𝑥) ∈ (Clsd‘𝐾))
32		fofun 6354	. . . . . . . . . . 11 ⊢ (𝐹:∪ 𝐽–onto→𝑌 → Fun 𝐹)
33		funcnvcnv 6189	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
34		imadif 6206	. . . . . . . . . . 11 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (𝑌 ∖ 𝑦)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝑦)))
35	18, 32, 33, 34	4syl 19	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ (𝑌 ∖ 𝑦)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝑦)))
36	12	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐹:∪ 𝐽⟶𝑌)
37		fimacnv 6596	. . . . . . . . . . . 12 ⊢ (𝐹:∪ 𝐽⟶𝑌 → (◡𝐹 “ 𝑌) = ∪ 𝐽)
38	36, 37	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑌) = ∪ 𝐽)
39	38	difeq1d 3954	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝑦)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝑦)))
40	35, 39	eqtrd 2861	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ (𝑌 ∖ 𝑦)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝑦)))
41	7	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐽 ∈ Top)
42		simprr 789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑦) ∈ 𝐽)
43	8	opncld 21208	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ 𝑦) ∈ 𝐽) → (∪ 𝐽 ∖ (◡𝐹 “ 𝑦)) ∈ (Clsd‘𝐽))
44	41, 42, 43	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (∪ 𝐽 ∖ (◡𝐹 “ 𝑦)) ∈ (Clsd‘𝐽))
45	40, 44	eqeltrd 2906	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ (𝑌 ∖ 𝑦)) ∈ (Clsd‘𝐽))
46	28, 31, 45	rspcdva 3532	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) ∈ (Clsd‘𝐾))
47	26, 46	eqeltrrd 2907	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (∪ 𝐾 ∖ 𝑦) ∈ (Clsd‘𝐾))
48		topontop 21088	. . . . . . . 8 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
49	22, 48	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐾 ∈ Top)
50		simprl 787	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ⊆ 𝑌)
51	50, 24	sseqtrd 3866	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ⊆ ∪ 𝐾)
52		eqid 2825	. . . . . . . 8 ⊢ ∪ 𝐾 = ∪ 𝐾
53	52	isopn2 21207	. . . . . . 7 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾) → (𝑦 ∈ 𝐾 ↔ (∪ 𝐾 ∖ 𝑦) ∈ (Clsd‘𝐾)))
54	49, 51, 53	syl2anc 579	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝑦 ∈ 𝐾 ↔ (∪ 𝐾 ∖ 𝑦) ∈ (Clsd‘𝐾)))
55	47, 54	mpbird 249	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ∈ 𝐾)
56	55	ex 403	. . . 4 ⊢ (𝜑 → ((𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽) → 𝑦 ∈ 𝐾))
57	17, 56	sylbid 232	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) → 𝑦 ∈ 𝐾))
58	57	ssrdv 3833	. 2 ⊢ (𝜑 → (𝐽 qTop 𝐹) ⊆ 𝐾)
59	5, 58	eqssd 3844	1 ⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ∀wral 3117   ∖ cdif 3795   ⊆ wss 3798  ∪ cuni 4658  ^◡ccnv 5341  ran crn 5343   “ cima 5345  Fun wfun 6117   Fn wfn 6118  ⟶wf 6119  –onto→wfo 6121  ‘cfv 6123  (class class class)co 6905   qTop cqtop 16516  Topctop 21068  TopOnctopon 21085  Clsdccld 21191   Cn ccn 21399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-map 8124  df-qtop 16520  df-top 21069  df-topon 21086  df-cld 21194  df-cn 21402

This theorem is referenced by: (None)