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

Theorem cnclima 19563
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  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( `' F " A )  e.  (
Clsd `  J )
)

Proof of Theorem cnclima
StepHypRef Expression
1 eqid 2467 . . . . . 6  |-  U. J  =  U. J
2 eqid 2467 . . . . . 6  |-  U. K  =  U. K
31, 2cnf 19541 . . . . 5  |-  ( F  e.  ( J  Cn  K )  ->  F : U. J --> U. K
)
43adantr 465 . . . 4  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  ->  F : U. J --> U. K
)
5 ffun 5733 . . . . . 6  |-  ( F : U. J --> U. K  ->  Fun  F )
6 funcnvcnv 5646 . . . . . 6  |-  ( Fun 
F  ->  Fun  `' `' F )
7 imadif 5663 . . . . . 6  |-  ( Fun  `' `' F  ->  ( `' F " ( U. K  \  A ) )  =  ( ( `' F " U. K
)  \  ( `' F " A ) ) )
85, 6, 73syl 20 . . . . 5  |-  ( F : U. J --> U. K  ->  ( `' F "
( U. K  \  A ) )  =  ( ( `' F " U. K )  \ 
( `' F " A ) ) )
9 fimacnv 6013 . . . . . 6  |-  ( F : U. J --> U. K  ->  ( `' F " U. K )  =  U. J )
109difeq1d 3621 . . . . 5  |-  ( F : U. J --> U. K  ->  ( ( `' F " U. K )  \ 
( `' F " A ) )  =  ( U. J  \ 
( `' F " A ) ) )
118, 10eqtr2d 2509 . . . 4  |-  ( F : U. J --> U. K  ->  ( U. J  \ 
( `' F " A ) )  =  ( `' F "
( U. K  \  A ) ) )
124, 11syl 16 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( U. J  \ 
( `' F " A ) )  =  ( `' F "
( U. K  \  A ) ) )
132cldopn 19326 . . . 4  |-  ( A  e.  ( Clsd `  K
)  ->  ( U. K  \  A )  e.  K )
14 cnima 19560 . . . 4  |-  ( ( F  e.  ( J  Cn  K )  /\  ( U. K  \  A
)  e.  K )  ->  ( `' F " ( U. K  \  A ) )  e.  J )
1513, 14sylan2 474 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( `' F "
( U. K  \  A ) )  e.  J )
1612, 15eqeltrd 2555 . 2  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( U. J  \ 
( `' F " A ) )  e.  J )
17 cntop1 19535 . . . 4  |-  ( F  e.  ( J  Cn  K )  ->  J  e.  Top )
1817adantr 465 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  ->  J  e.  Top )
19 cnvimass 5357 . . . 4  |-  ( `' F " A ) 
C_  dom  F
20 fdm 5735 . . . . 5  |-  ( F : U. J --> U. K  ->  dom  F  =  U. J )
214, 20syl 16 . . . 4  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  ->  dom  F  =  U. J
)
2219, 21syl5sseq 3552 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( `' F " A )  C_  U. J
)
231iscld2 19323 . . 3  |-  ( ( J  e.  Top  /\  ( `' F " A ) 
C_  U. J )  -> 
( ( `' F " A )  e.  (
Clsd `  J )  <->  ( U. J  \  ( `' F " A ) )  e.  J ) )
2418, 22, 23syl2anc 661 . 2  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( ( `' F " A )  e.  (
Clsd `  J )  <->  ( U. J  \  ( `' F " A ) )  e.  J ) )
2516, 24mpbird 232 1  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  ( Clsd `  K ) )  -> 
( `' F " A )  e.  (
Clsd `  J )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767    \ cdif 3473    C_ wss 3476   U.cuni 4245   `'ccnv 4998   dom cdm 4999   "cima 5002   Fun wfun 5582   -->wf 5584   ` cfv 5588  (class class class)co 6284   Topctop 19189   Clsdccld 19311    Cn ccn 19519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-map 7422  df-top 19194  df-topon 19197  df-cld 19314  df-cn 19522
This theorem is referenced by:  iscncl  19564  cncls2i  19565  paste  19589  cnt1  19645  dnsconst  19673  cnconn  19717  hauseqlcld  19910  txcon  19953  imasncld  19955  r0cld  20002  kqreglem2  20006  kqnrmlem1  20007  kqnrmlem2  20008  hmeocld  20031  nrmhmph  20058  tgphaus  20378  csscld  21452  clsocv  21453  hmeoclda  29756  hmeocldb  29757  rfcnpre3  31014  rfcnpre4  31015
  Copyright terms: Public domain W3C validator