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

Theorem cnima 16994
Description: An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)
Assertion
Ref Expression
cnima  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  K )  ->  ( `' F " A )  e.  J
)

Proof of Theorem cnima
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqid 2283 . . . . 5  |-  U. J  =  U. J
2 eqid 2283 . . . . 5  |-  U. K  =  U. K
31, 2iscn2 16968 . . . 4  |-  ( F  e.  ( J  Cn  K )  <->  ( ( J  e.  Top  /\  K  e.  Top )  /\  ( F : U. J --> U. K  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
43simprbi 450 . . 3  |-  ( F  e.  ( J  Cn  K )  ->  ( F : U. J --> U. K  /\  A. x  e.  K  ( `' F " x )  e.  J ) )
54simprd 449 . 2  |-  ( F  e.  ( J  Cn  K )  ->  A. x  e.  K  ( `' F " x )  e.  J )
6 imaeq2 5008 . . . 4  |-  ( x  =  A  ->  ( `' F " x )  =  ( `' F " A ) )
76eleq1d 2349 . . 3  |-  ( x  =  A  ->  (
( `' F "
x )  e.  J  <->  ( `' F " A )  e.  J ) )
87rspccva 2883 . 2  |-  ( ( A. x  e.  K  ( `' F " x )  e.  J  /\  A  e.  K )  ->  ( `' F " A )  e.  J )
95, 8sylan 457 1  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  K )  ->  ( `' F " A )  e.  J
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543   U.cuni 3827   `'ccnv 4688   "cima 4692   -->wf 5251  (class class class)co 5858   Topctop 16631    Cn ccn 16954
This theorem is referenced by:  cnco  16995  cnclima  16997  cnntri  17000  cnss1  17005  cnss2  17006  cncnpi  17007  cnrest  17013  cnt0  17074  cnhaus  17082  cncmp  17119  cnconn  17148  2ndcomap  17184  kgencn3  17253  txcnmpt  17318  txdis1cn  17329  pthaus  17332  ptrescn  17333  txkgen  17346  xkoco2cn  17352  xkococnlem  17353  txcon  17383  qtopkgen  17401  qtopss  17406  isr0  17428  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  hmeoima  17456  hmeoopn  17457  hmeoimaf1o  17461  reghmph  17484  nrmhmph  17485  tmdgsum2  17779  symgtgp  17784  ghmcnp  17797  tgpt0  17801  divstgpopn  17802  divstgplem  17803  nmhmcn  18601  mbfimaopnlem  19010  cncombf  19013  cnmbf  19014  dvloglem  19995  efopnlem2  20004  efopn  20005  atansopn  20228  cnmbfm  23568  cvmsss2  23805  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem9a  23834  cvmlift2lem9  23842  cvmlift2lem10  23843  cvmlift3lem6  23855  cvmlift3lem8  23857  intopcoaconc  25541  prcnt  25551  rfcnpre1  27690  rfcnpre2  27702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-map 6774  df-top 16636  df-topon 16639  df-cn 16957
  Copyright terms: Public domain W3C validator