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

Theorem cnima 21879
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 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴𝐾) → (𝐹𝐴) ∈ 𝐽)

Proof of Theorem cnima
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2824 . . . . 5 𝐽 = 𝐽
2 eqid 2824 . . . . 5 𝐾 = 𝐾
31, 2iscn2 21852 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹: 𝐽 𝐾 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
43simprbi 500 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹: 𝐽 𝐾 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
54simprd 499 . 2 (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)
6 imaeq2 5914 . . . 4 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
76eleq1d 2900 . . 3 (𝑥 = 𝐴 → ((𝐹𝑥) ∈ 𝐽 ↔ (𝐹𝐴) ∈ 𝐽))
87rspccva 3608 . 2 ((∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽𝐴𝐾) → (𝐹𝐴) ∈ 𝐽)
95, 8sylan 583 1 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴𝐾) → (𝐹𝐴) ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115  wral 3133   cuni 4824  ccnv 5542  cima 5546  wf 6341  (class class class)co 7151  Topctop 21507   Cn ccn 21838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-fv 6353  df-ov 7154  df-oprab 7155  df-mpo 7156  df-map 8406  df-top 21508  df-topon 21525  df-cn 21841
This theorem is referenced by:  cnco  21880  cnclima  21882  cnntri  21885  cnss1  21890  cnss2  21891  cncnpi  21892  cnrest  21899  cnt0  21960  cnhaus  21968  cncmp  22006  cnconn  22036  2ndcomap  22072  kgencn3  22172  txcnmpt  22238  txdis1cn  22249  pthaus  22252  ptrescn  22253  txkgen  22266  xkoco2cn  22272  xkococnlem  22273  txconn  22303  imasnopn  22304  qtopkgen  22324  qtopss  22329  isr0  22351  kqreglem1  22355  kqreglem2  22356  kqnrmlem1  22357  kqnrmlem2  22358  hmeoima  22379  hmeoopn  22380  hmeoimaf1o  22384  reghmph  22407  nrmhmph  22408  tmdgsum2  22710  symgtgp  22720  ghmcnp  22729  tgpt0  22733  qustgpopn  22734  qustgplem  22735  nmhmcn  23734  mbfimaopnlem  24268  cncombf  24271  cnmbf  24272  dvloglem  25248  efopnlem2  25257  efopn  25258  atansopn  25527  cnmbfm  31606  cvmsss2  32606  cvmliftmolem2  32614  cvmliftlem15  32630  cvmlift2lem9a  32635  cvmlift2lem9  32643  cvmlift2lem10  32644  cvmlift3lem6  32656  cvmlift3lem8  32658  dvtanlem  35078  rfcnpre1  41596  rfcnpre2  41608  icccncfext  42482
  Copyright terms: Public domain W3C validator