Theorem cnima 22414

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542   ∈ wcel 2110  ∀wral 3066  ∪ cuni 4845  ^◡ccnv 5589   “ cima 5593  ⟶wf 6428  (class class class)co 7271  Topctop 22040   Cn ccn 22373

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-map 8600  df-top 22041  df-topon 22058  df-cn 22376

This theorem is referenced by:  cnco  22415  cnclima  22417  cnntri  22420  cnss1  22425  cnss2  22426  cncnpi  22427  cnrest  22434  cnt0  22495  cnhaus  22503  cncmp  22541  cnconn  22571  2ndcomap  22607  kgencn3  22707  txcnmpt  22773  txdis1cn  22784  pthaus  22787  ptrescn  22788  txkgen  22801  xkoco2cn  22807  xkococnlem  22808  txconn  22838  imasnopn  22839  qtopkgen  22859  qtopss  22864  isr0  22886  kqreglem1  22890  kqreglem2  22891  kqnrmlem1  22892  kqnrmlem2  22893  hmeoima  22914  hmeoopn  22915  hmeoimaf1o  22919  reghmph  22942  nrmhmph  22943  tmdgsum2  23245  symgtgp  23255  ghmcnp  23264  tgpt0  23268  qustgpopn  23269  qustgplem  23270  nmhmcn  24281  mbfimaopnlem  24817  cncombf  24820  cnmbf  24821  dvloglem  25801  efopnlem2  25810  efopn  25811  atansopn  26080  cnmbfm  32226  cvmsss2  33232  cvmliftmolem2  33240  cvmliftlem15  33256  cvmlift2lem9a  33261  cvmlift2lem9  33269  cvmlift2lem10  33270  cvmlift3lem6  33282  cvmlift3lem8  33284  dvtanlem  35822  rfcnpre1  42532  rfcnpre2  42544  icccncfext  43399