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

Theorem cnima 18869
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 2443 . . . . 5  |-  U. J  =  U. J
2 eqid 2443 . . . . 5  |-  U. K  =  U. K
31, 2iscn2 18842 . . . 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 464 . . 3  |-  ( F  e.  ( J  Cn  K )  ->  ( F : U. J --> U. K  /\  A. x  e.  K  ( `' F " x )  e.  J ) )
54simprd 463 . 2  |-  ( F  e.  ( J  Cn  K )  ->  A. x  e.  K  ( `' F " x )  e.  J )
6 imaeq2 5165 . . . 4  |-  ( x  =  A  ->  ( `' F " x )  =  ( `' F " A ) )
76eleq1d 2509 . . 3  |-  ( x  =  A  ->  (
( `' F "
x )  e.  J  <->  ( `' F " A )  e.  J ) )
87rspccva 3072 . 2  |-  ( ( A. x  e.  K  ( `' F " x )  e.  J  /\  A  e.  K )  ->  ( `' F " A )  e.  J )
95, 8sylan 471 1  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  K )  ->  ( `' F " A )  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2715   U.cuni 4091   `'ccnv 4839   "cima 4843   -->wf 5414  (class class class)co 6091   Topctop 18498    Cn ccn 18828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-map 7216  df-top 18503  df-topon 18506  df-cn 18831
This theorem is referenced by:  cnco  18870  cnclima  18872  cnntri  18875  cnss1  18880  cnss2  18881  cncnpi  18882  cnrest  18889  cnt0  18950  cnhaus  18958  cncmp  18995  cnconn  19026  2ndcomap  19062  kgencn3  19131  txcnmpt  19197  txdis1cn  19208  pthaus  19211  ptrescn  19212  txkgen  19225  xkoco2cn  19231  xkococnlem  19232  txcon  19262  imasnopn  19263  qtopkgen  19283  qtopss  19288  isr0  19310  kqreglem1  19314  kqreglem2  19315  kqnrmlem1  19316  kqnrmlem2  19317  hmeoima  19338  hmeoopn  19339  hmeoimaf1o  19343  reghmph  19366  nrmhmph  19367  tmdgsum2  19667  symgtgp  19672  ghmcnp  19685  tgpt0  19689  divstgpopn  19690  divstgplem  19691  nmhmcn  20675  mbfimaopnlem  21133  cncombf  21136  cnmbf  21137  dvloglem  22093  efopnlem2  22102  efopn  22103  atansopn  22327  cnmbfm  26678  cvmsss2  27163  cvmliftmolem2  27171  cvmliftlem15  27187  cvmlift2lem9a  27192  cvmlift2lem9  27200  cvmlift2lem10  27201  cvmlift3lem6  27213  cvmlift3lem8  27215  rfcnpre1  29741  rfcnpre2  29753
  Copyright terms: Public domain W3C validator