Theorem cnima 23203

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ∪ cuni 4883  ^◡ccnv 5653   “ cima 5657  ⟶wf 6527  (class class class)co 7405  Topctop 22831   Cn ccn 23162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8842  df-top 22832  df-topon 22849  df-cn 23165

This theorem is referenced by:  cnco  23204  cnclima  23206  cnntri  23209  cnss1  23214  cnss2  23215  cncnpi  23216  cnrest  23223  cnt0  23284  cnhaus  23292  cncmp  23330  cnconn  23360  2ndcomap  23396  kgencn3  23496  txcnmpt  23562  txdis1cn  23573  pthaus  23576  ptrescn  23577  txkgen  23590  xkoco2cn  23596  xkococnlem  23597  txconn  23627  imasnopn  23628  qtopkgen  23648  qtopss  23653  isr0  23675  kqreglem1  23679  kqreglem2  23680  kqnrmlem1  23681  kqnrmlem2  23682  hmeoima  23703  hmeoopn  23704  hmeoimaf1o  23708  reghmph  23731  nrmhmph  23732  tmdgsum2  24034  symgtgp  24044  ghmcnp  24053  tgpt0  24057  qustgpopn  24058  qustgplem  24059  nmhmcn  25071  mbfimaopnlem  25608  cncombf  25611  cnmbf  25612  dvloglem  26609  efopnlem2  26618  efopn  26619  atansopn  26894  cnmbfm  34295  cvmsss2  35296  cvmliftmolem2  35304  cvmliftlem15  35320  cvmlift2lem9a  35325  cvmlift2lem9  35333  cvmlift2lem10  35334  cvmlift3lem6  35346  cvmlift3lem8  35348  dvtanlem  37693  resuppsinopn  42406  rfcnpre1  45043  rfcnpre2  45055  icccncfext  45916