Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  qtopcmap Structured version   Visualization version   GIF version

Theorem qtopcmap 21332
 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.
StepHypRef Expression
1 qtopomap.5 . . 3 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
2 qtopomap.4 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
3 qtopomap.6 . . 3 (𝜑 → ran 𝐹 = 𝑌)
4 qtopss 21328 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 = 𝑌) → 𝐾 ⊆ (𝐽 qTop 𝐹))
51, 2, 3, 4syl3anc 1318 . 2 (𝜑𝐾 ⊆ (𝐽 qTop 𝐹))
6 cntop1 20854 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
71, 6syl 17 . . . . 5 (𝜑𝐽 ∈ Top)
8 eqid 2610 . . . . . . . . . 10 𝐽 = 𝐽
98toptopon 20548 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
107, 9sylib 207 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
11 cnf2 20863 . . . . . . . 8 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹: 𝐽𝑌)
1210, 2, 1, 11syl3anc 1318 . . . . . . 7 (𝜑𝐹: 𝐽𝑌)
13 ffn 5958 . . . . . . 7 (𝐹: 𝐽𝑌𝐹 Fn 𝐽)
1412, 13syl 17 . . . . . 6 (𝜑𝐹 Fn 𝐽)
15 df-fo 5810 . . . . . 6 (𝐹: 𝐽onto𝑌 ↔ (𝐹 Fn 𝐽 ∧ ran 𝐹 = 𝑌))
1614, 3, 15sylanbrc 695 . . . . 5 (𝜑𝐹: 𝐽onto𝑌)
178elqtop2 21314 . . . . 5 ((𝐽 ∈ Top ∧ 𝐹: 𝐽onto𝑌) → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)))
187, 16, 17syl2anc 691 . . . 4 (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)))
1916adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝐹: 𝐽onto𝑌)
20 difss 3699 . . . . . . . . 9 (𝑌𝑦) ⊆ 𝑌
21 foimacnv 6067 . . . . . . . . 9 ((𝐹: 𝐽onto𝑌 ∧ (𝑌𝑦) ⊆ 𝑌) → (𝐹 “ (𝐹 “ (𝑌𝑦))) = (𝑌𝑦))
2219, 20, 21sylancl 693 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹 “ (𝐹 “ (𝑌𝑦))) = (𝑌𝑦))
232adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝐾 ∈ (TopOn‘𝑌))
24 toponuni 20542 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
2523, 24syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝑌 = 𝐾)
2625difeq1d 3689 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝑌𝑦) = ( 𝐾𝑦))
2722, 26eqtrd 2644 . . . . . . 7 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹 “ (𝐹 “ (𝑌𝑦))) = ( 𝐾𝑦))
28 fofun 6029 . . . . . . . . . . 11 (𝐹: 𝐽onto𝑌 → Fun 𝐹)
29 funcnvcnv 5870 . . . . . . . . . . 11 (Fun 𝐹 → Fun 𝐹)
30 imadif 5887 . . . . . . . . . . 11 (Fun 𝐹 → (𝐹 “ (𝑌𝑦)) = ((𝐹𝑌) ∖ (𝐹𝑦)))
3119, 28, 29, 304syl 19 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹 “ (𝑌𝑦)) = ((𝐹𝑌) ∖ (𝐹𝑦)))
3212adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝐹: 𝐽𝑌)
33 fimacnv 6255 . . . . . . . . . . . 12 (𝐹: 𝐽𝑌 → (𝐹𝑌) = 𝐽)
3432, 33syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹𝑌) = 𝐽)
3534difeq1d 3689 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → ((𝐹𝑌) ∖ (𝐹𝑦)) = ( 𝐽 ∖ (𝐹𝑦)))
3631, 35eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹 “ (𝑌𝑦)) = ( 𝐽 ∖ (𝐹𝑦)))
377adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝐽 ∈ Top)
38 simprr 792 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹𝑦) ∈ 𝐽)
398opncld 20647 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐹𝑦) ∈ 𝐽) → ( 𝐽 ∖ (𝐹𝑦)) ∈ (Clsd‘𝐽))
4037, 38, 39syl2anc 691 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → ( 𝐽 ∖ (𝐹𝑦)) ∈ (Clsd‘𝐽))
4136, 40eqeltrd 2688 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹 “ (𝑌𝑦)) ∈ (Clsd‘𝐽))
42 qtopcmap.7 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → (𝐹𝑥) ∈ (Clsd‘𝐾))
4342ralrimiva 2949 . . . . . . . . 9 (𝜑 → ∀𝑥 ∈ (Clsd‘𝐽)(𝐹𝑥) ∈ (Clsd‘𝐾))
4443adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → ∀𝑥 ∈ (Clsd‘𝐽)(𝐹𝑥) ∈ (Clsd‘𝐾))
45 imaeq2 5381 . . . . . . . . . 10 (𝑥 = (𝐹 “ (𝑌𝑦)) → (𝐹𝑥) = (𝐹 “ (𝐹 “ (𝑌𝑦))))
4645eleq1d 2672 . . . . . . . . 9 (𝑥 = (𝐹 “ (𝑌𝑦)) → ((𝐹𝑥) ∈ (Clsd‘𝐾) ↔ (𝐹 “ (𝐹 “ (𝑌𝑦))) ∈ (Clsd‘𝐾)))
4746rspcv 3278 . . . . . . . 8 ((𝐹 “ (𝑌𝑦)) ∈ (Clsd‘𝐽) → (∀𝑥 ∈ (Clsd‘𝐽)(𝐹𝑥) ∈ (Clsd‘𝐾) → (𝐹 “ (𝐹 “ (𝑌𝑦))) ∈ (Clsd‘𝐾)))
4841, 44, 47sylc 63 . . . . . . 7 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝐹 “ (𝐹 “ (𝑌𝑦))) ∈ (Clsd‘𝐾))
4927, 48eqeltrrd 2689 . . . . . 6 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → ( 𝐾𝑦) ∈ (Clsd‘𝐾))
50 topontop 20541 . . . . . . . 8 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
5123, 50syl 17 . . . . . . 7 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝐾 ∈ Top)
52 simprl 790 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝑦𝑌)
5352, 25sseqtrd 3604 . . . . . . 7 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝑦 𝐾)
54 eqid 2610 . . . . . . . 8 𝐾 = 𝐾
5554isopn2 20646 . . . . . . 7 ((𝐾 ∈ Top ∧ 𝑦 𝐾) → (𝑦𝐾 ↔ ( 𝐾𝑦) ∈ (Clsd‘𝐾)))
5651, 53, 55syl2anc 691 . . . . . 6 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → (𝑦𝐾 ↔ ( 𝐾𝑦) ∈ (Clsd‘𝐾)))
5749, 56mpbird 246 . . . . 5 ((𝜑 ∧ (𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽)) → 𝑦𝐾)
5857ex 449 . . . 4 (𝜑 → ((𝑦𝑌 ∧ (𝐹𝑦) ∈ 𝐽) → 𝑦𝐾))
5918, 58sylbid 229 . . 3 (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) → 𝑦𝐾))
6059ssrdv 3574 . 2 (𝜑 → (𝐽 qTop 𝐹) ⊆ 𝐾)
615, 60eqssd 3585 1 (𝜑𝐾 = (𝐽 qTop 𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ∖ cdif 3537   ⊆ wss 3540  ∪ cuni 4372  ◡ccnv 5037  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549   qTop cqtop 15986  Topctop 20517  TopOnctopon 20518  Clsdccld 20630   Cn ccn 20838 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746  df-qtop 15990  df-top 20521  df-topon 20523  df-cld 20633  df-cn 20841 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator