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

Theorem cnclima 23276
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 2737 . . . . . 6 𝐽 = 𝐽
2 eqid 2737 . . . . . 6 𝐾 = 𝐾
31, 2cnf 23254 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
43adantr 480 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → 𝐹: 𝐽 𝐾)
5 ffun 6739 . . . . . 6 (𝐹: 𝐽 𝐾 → Fun 𝐹)
6 funcnvcnv 6633 . . . . . 6 (Fun 𝐹 → Fun 𝐹)
7 imadif 6650 . . . . . 6 (Fun 𝐹 → (𝐹 “ ( 𝐾𝐴)) = ((𝐹 𝐾) ∖ (𝐹𝐴)))
85, 6, 73syl 18 . . . . 5 (𝐹: 𝐽 𝐾 → (𝐹 “ ( 𝐾𝐴)) = ((𝐹 𝐾) ∖ (𝐹𝐴)))
9 fimacnv 6758 . . . . . 6 (𝐹: 𝐽 𝐾 → (𝐹 𝐾) = 𝐽)
109difeq1d 4125 . . . . 5 (𝐹: 𝐽 𝐾 → ((𝐹 𝐾) ∖ (𝐹𝐴)) = ( 𝐽 ∖ (𝐹𝐴)))
118, 10eqtr2d 2778 . . . 4 (𝐹: 𝐽 𝐾 → ( 𝐽 ∖ (𝐹𝐴)) = (𝐹 “ ( 𝐾𝐴)))
124, 11syl 17 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → ( 𝐽 ∖ (𝐹𝐴)) = (𝐹 “ ( 𝐾𝐴)))
132cldopn 23039 . . . 4 (𝐴 ∈ (Clsd‘𝐾) → ( 𝐾𝐴) ∈ 𝐾)
14 cnima 23273 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ ( 𝐾𝐴) ∈ 𝐾) → (𝐹 “ ( 𝐾𝐴)) ∈ 𝐽)
1513, 14sylan2 593 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹 “ ( 𝐾𝐴)) ∈ 𝐽)
1612, 15eqeltrd 2841 . 2 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → ( 𝐽 ∖ (𝐹𝐴)) ∈ 𝐽)
17 cntop1 23248 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
18 cnvimass 6100 . . . 4 (𝐹𝐴) ⊆ dom 𝐹
1918, 4fssdm 6755 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹𝐴) ⊆ 𝐽)
201iscld2 23036 . . 3 ((𝐽 ∈ Top ∧ (𝐹𝐴) ⊆ 𝐽) → ((𝐹𝐴) ∈ (Clsd‘𝐽) ↔ ( 𝐽 ∖ (𝐹𝐴)) ∈ 𝐽))
2117, 19, 20syl2an2r 685 . 2 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → ((𝐹𝐴) ∈ (Clsd‘𝐽) ↔ ( 𝐽 ∖ (𝐹𝐴)) ∈ 𝐽))
2216, 21mpbird 257 1 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (𝐹𝐴) ∈ (Clsd‘𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  cdif 3948  wss 3951   cuni 4907  ccnv 5684  cima 5688  Fun wfun 6555  wf 6557  cfv 6561  (class class class)co 7431  Topctop 22899  Clsdccld 23024   Cn ccn 23232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-top 22900  df-topon 22917  df-cld 23027  df-cn 23235
This theorem is referenced by:  iscncl  23277  cncls2i  23278  paste  23302  cnt1  23358  dnsconst  23386  cnconn  23430  hauseqlcld  23654  txconn  23697  imasncld  23699  r0cld  23746  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  hmeocld  23775  nrmhmph  23802  tgphaus  24125  csscld  25283  clsocv  25284  hmeoclda  36334  hmeocldb  36335  rfcnpre3  45038  rfcnpre4  45039  sepfsepc  48825  seppcld  48827
  Copyright terms: Public domain W3C validator