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

Theorem cnima 20291
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 2451 . . . . 5  |-  U. J  =  U. J
2 eqid 2451 . . . . 5  |-  U. K  =  U. K
31, 2iscn2 20264 . . . 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 470 . . 3  |-  ( F  e.  ( J  Cn  K )  ->  ( F : U. J --> U. K  /\  A. x  e.  K  ( `' F " x )  e.  J ) )
54simprd 469 . 2  |-  ( F  e.  ( J  Cn  K )  ->  A. x  e.  K  ( `' F " x )  e.  J )
6 imaeq2 5141 . . . 4  |-  ( x  =  A  ->  ( `' F " x )  =  ( `' F " A ) )
76eleq1d 2513 . . 3  |-  ( x  =  A  ->  (
( `' F "
x )  e.  J  <->  ( `' F " A )  e.  J ) )
87rspccva 3116 . 2  |-  ( ( A. x  e.  K  ( `' F " x )  e.  J  /\  A  e.  K )  ->  ( `' F " A )  e.  J )
95, 8sylan 478 1  |-  ( ( F  e.  ( J  Cn  K )  /\  A  e.  K )  ->  ( `' F " A )  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1447    e. wcel 1890   A.wral 2736   U.cuni 4167   `'ccnv 4810   "cima 4814   -->wf 5556  (class class class)co 6275   Topctop 19927    Cn ccn 20250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-fv 5568  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-map 7460  df-top 19931  df-topon 19933  df-cn 20253
This theorem is referenced by:  cnco  20292  cnclima  20294  cnntri  20297  cnss1  20302  cnss2  20303  cncnpi  20304  cnrest  20311  cnt0  20372  cnhaus  20380  cncmp  20417  cnconn  20447  2ndcomap  20483  kgencn3  20583  txcnmpt  20649  txdis1cn  20660  pthaus  20663  ptrescn  20664  txkgen  20677  xkoco2cn  20683  xkococnlem  20684  txcon  20714  imasnopn  20715  qtopkgen  20735  qtopss  20740  isr0  20762  kqreglem1  20766  kqreglem2  20767  kqnrmlem1  20768  kqnrmlem2  20769  hmeoima  20790  hmeoopn  20791  hmeoimaf1o  20795  reghmph  20818  nrmhmph  20819  tmdgsum2  21121  symgtgp  21126  ghmcnp  21139  tgpt0  21143  qustgpopn  21144  qustgplem  21145  nmhmcn  22144  mbfimaopnlem  22622  cncombf  22625  cnmbf  22626  dvloglem  23604  efopnlem2  23613  efopn  23614  atansopn  23869  cnmbfm  29090  cvmsss2  30002  cvmliftmolem2  30010  cvmliftlem15  30026  cvmlift2lem9a  30031  cvmlift2lem9  30039  cvmlift2lem10  30040  cvmlift3lem6  30052  cvmlift3lem8  30054  dvtanlem  31991  rfcnpre1  37336  rfcnpre2  37348  icccncfext  37806
  Copyright terms: Public domain W3C validator