Theorem cnima 22416

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 2738	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid 2738	. . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	iscn2 22389	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simprbi 497	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))
5	4	simprd 496	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)
6		imaeq2 5965	. . . 4 ⊢ (𝑥 = 𝐴 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝐴))
7	6	eleq1d 2823	. . 3 ⊢ (𝑥 = 𝐴 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ 𝐽))
8	7	rspccva 3560	. 2 ⊢ ((∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)
9	5, 8	sylan 580	1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∪ cuni 4839  ^◡ccnv 5588   “ cima 5592  ⟶wf 6429  (class class class)co 7275  Topctop 22042   Cn ccn 22375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-map 8617  df-top 22043  df-topon 22060  df-cn 22378

This theorem is referenced by:  cnco  22417  cnclima  22419  cnntri  22422  cnss1  22427  cnss2  22428  cncnpi  22429  cnrest  22436  cnt0  22497  cnhaus  22505  cncmp  22543  cnconn  22573  2ndcomap  22609  kgencn3  22709  txcnmpt  22775  txdis1cn  22786  pthaus  22789  ptrescn  22790  txkgen  22803  xkoco2cn  22809  xkococnlem  22810  txconn  22840  imasnopn  22841  qtopkgen  22861  qtopss  22866  isr0  22888  kqreglem1  22892  kqreglem2  22893  kqnrmlem1  22894  kqnrmlem2  22895  hmeoima  22916  hmeoopn  22917  hmeoimaf1o  22921  reghmph  22944  nrmhmph  22945  tmdgsum2  23247  symgtgp  23257  ghmcnp  23266  tgpt0  23270  qustgpopn  23271  qustgplem  23272  nmhmcn  24283  mbfimaopnlem  24819  cncombf  24822  cnmbf  24823  dvloglem  25803  efopnlem2  25812  efopn  25813  atansopn  26082  cnmbfm  32230  cvmsss2  33236  cvmliftmolem2  33244  cvmliftlem15  33260  cvmlift2lem9a  33265  cvmlift2lem9  33273  cvmlift2lem10  33274  cvmlift3lem6  33286  cvmlift3lem8  33288  dvtanlem  35826  rfcnpre1  42562  rfcnpre2  42574  icccncfext  43428