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

Theorem cnclima 21274
 Description: A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnclima ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹𝐴) ∈ (Clsd‘𝐽))

Proof of Theorem cnclima
StepHypRef Expression
1 eqid 2760 . . . . . 6 𝐽 = 𝐽
2 eqid 2760 . . . . . 6 𝐾 = 𝐾
31, 2cnf 21252 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
43adantr 472 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → 𝐹: 𝐽 𝐾)
5 ffun 6209 . . . . . 6 (𝐹: 𝐽 𝐾 → Fun 𝐹)
6 funcnvcnv 6117 . . . . . 6 (Fun 𝐹 → Fun 𝐹)
7 imadif 6134 . . . . . 6 (Fun 𝐹 → (𝐹 “ ( 𝐾𝐴)) = ((𝐹 𝐾) ∖ (𝐹𝐴)))
85, 6, 73syl 18 . . . . 5 (𝐹: 𝐽 𝐾 → (𝐹 “ ( 𝐾𝐴)) = ((𝐹 𝐾) ∖ (𝐹𝐴)))
9 fimacnv 6510 . . . . . 6 (𝐹: 𝐽 𝐾 → (𝐹 𝐾) = 𝐽)
109difeq1d 3870 . . . . 5 (𝐹: 𝐽 𝐾 → ((𝐹 𝐾) ∖ (𝐹𝐴)) = ( 𝐽 ∖ (𝐹𝐴)))
118, 10eqtr2d 2795 . . . 4 (𝐹: 𝐽 𝐾 → ( 𝐽 ∖ (𝐹𝐴)) = (𝐹 “ ( 𝐾𝐴)))
124, 11syl 17 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → ( 𝐽 ∖ (𝐹𝐴)) = (𝐹 “ ( 𝐾𝐴)))
132cldopn 21037 . . . 4 (𝐴 ∈ (Clsd‘𝐾) → ( 𝐾𝐴) ∈ 𝐾)
14 cnima 21271 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ ( 𝐾𝐴) ∈ 𝐾) → (𝐹 “ ( 𝐾𝐴)) ∈ 𝐽)
1513, 14sylan2 492 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹 “ ( 𝐾𝐴)) ∈ 𝐽)
1612, 15eqeltrd 2839 . 2 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → ( 𝐽 ∖ (𝐹𝐴)) ∈ 𝐽)
17 cntop1 21246 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
1817adantr 472 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → 𝐽 ∈ Top)
19 cnvimass 5643 . . . 4 (𝐹𝐴) ⊆ dom 𝐹
20 fdm 6212 . . . . 5 (𝐹: 𝐽 𝐾 → dom 𝐹 = 𝐽)
214, 20syl 17 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → dom 𝐹 = 𝐽)
2219, 21syl5sseq 3794 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹𝐴) ⊆ 𝐽)
231iscld2 21034 . . 3 ((𝐽 ∈ Top ∧ (𝐹𝐴) ⊆ 𝐽) → ((𝐹𝐴) ∈ (Clsd‘𝐽) ↔ ( 𝐽 ∖ (𝐹𝐴)) ∈ 𝐽))
2418, 22, 23syl2anc 696 . 2 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → ((𝐹𝐴) ∈ (Clsd‘𝐽) ↔ ( 𝐽 ∖ (𝐹𝐴)) ∈ 𝐽))
2516, 24mpbird 247 1 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹𝐴) ∈ (Clsd‘𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ∖ cdif 3712   ⊆ wss 3715  ∪ cuni 4588  ◡ccnv 5265  dom cdm 5266   “ cima 5269  Fun wfun 6043  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813  Topctop 20900  Clsdccld 21022   Cn ccn 21230 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-map 8025  df-top 20901  df-topon 20918  df-cld 21025  df-cn 21233 This theorem is referenced by:  iscncl  21275  cncls2i  21276  paste  21300  cnt1  21356  dnsconst  21384  cnconn  21427  hauseqlcld  21651  txconn  21694  imasncld  21696  r0cld  21743  kqreglem2  21747  kqnrmlem1  21748  kqnrmlem2  21749  hmeocld  21772  nrmhmph  21799  tgphaus  22121  csscld  23248  clsocv  23249  hmeoclda  32634  hmeocldb  32635  rfcnpre3  39691  rfcnpre4  39692
 Copyright terms: Public domain W3C validator