Theorem cnima 23248

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.

Step	Hyp	Ref	Expression
1		eqid 2739	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid 2739	. . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	iscn2 23221	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simprbi 498	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))
5	4	simprd 496	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)
6		imaeq2 6008	. . . 4 ⊢ (𝑥 = 𝐴 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝐴))
7	6	eleq1d 2824	. . 3 ⊢ (𝑥 = 𝐴 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ 𝐽))
8	7	rspccva 3559	. 2 ⊢ ((∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)
9	5, 8	sylan 586	1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∪ cuni 4838  ^◡ccnv 5617   “ cima 5621  ⟶wf 6481  (class class class)co 7356  Topctop 22876   Cn ccn 23207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-map 8765  df-top 22877  df-topon 22894  df-cn 23210

This theorem is referenced by:  cnco  23249  cnclima  23251  cnntri  23254  cnss1  23259  cnss2  23260  cncnpi  23261  cnrest  23268  cnt0  23329  cnhaus  23337  cncmp  23375  cnconn  23405  2ndcomap  23441  kgencn3  23541  txcnmpt  23607  txdis1cn  23618  pthaus  23621  ptrescn  23622  txkgen  23635  xkoco2cn  23641  xkococnlem  23642  txconn  23672  imasnopn  23673  qtopkgen  23693  qtopss  23698  isr0  23720  kqreglem1  23724  kqreglem2  23725  kqnrmlem1  23726  kqnrmlem2  23727  hmeoima  23748  hmeoopn  23749  hmeoimaf1o  23753  reghmph  23776  nrmhmph  23777  tmdgsum2  24079  symgtgp  24089  ghmcnp  24098  tgpt0  24102  qustgpopn  24103  qustgplem  24104  nmhmcn  25105  mbfimaopnlem  25640  cncombf  25643  cnmbf  25644  dvloglem  26630  efopnlem2  26639  efopn  26640  atansopn  26914  cnmbfm  34447  cvmsss2  35502  cvmliftmolem2  35510  cvmliftlem15  35526  cvmlift2lem9a  35531  cvmlift2lem9  35539  cvmlift2lem10  35540  cvmlift3lem6  35552  cvmlift3lem8  35554  dvtanlem  38036  resuppsinopn  42840  rfcnpre1  45467  rfcnpre2  45479  icccncfext  46330