Theorem cnima 23496

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 2762	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid 2762	. . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	iscn2 23469	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simprbi 503	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))
5	4	simprd 501	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)
6		imaeq2 6056	. . . 4 ⊢ (𝑥 = 𝐴 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝐴))
7	6	eleq1d 2847	. . 3 ⊢ (𝑥 = 𝐴 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ 𝐽))
8	7	rspccva 3578	. 2 ⊢ ((∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)
9	5, 8	sylan 592	1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∪ cuni 4870  ^◡ccnv 5658   “ cima 5662  ⟶wf 6533  (class class class)co 7417  Topctop 23124   Cn ccn 23455

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-map 8832  df-top 23125  df-topon 23142  df-cn 23458

This theorem is used by:  cnco  23497  cnclima  23499  cnntri  23502  cnss1  23507  cnss2  23508  cncnpi  23509  cnrest  23516  cnt0  23577  cnhaus  23585  cncmp  23623  cnconn  23653  2ndcomap  23690  kgencn3  23790  txcnmpt  23856  txdis1cn  23867  pthaus  23870  ptrescn  23871  txkgen  23884  xkoco2cn  23890  xkococnlem  23891  txconn  23921  imasnopn  23922  qtopkgen  23942  qtopss  23947  isr0  23969  kqreglem1  23973  kqreglem2  23974  kqnrmlem1  23975  kqnrmlem2  23976  hmeoima  23997  hmeoopn  23998  hmeoimaf1o  24002  reghmph  24025  nrmhmph  24026  tmdgsum2  24328  symgtgp  24338  ghmcnp  24347  tgpt0  24351  qustgpopn  24352  qustgplem  24353  nmhmcn  25354  mbfimaopnlem  25889  cncombf  25892  cnmbf  25893  dvloglem  26893  efopnlem2  26902  efopn  26903  atansopn  27177  cnmbfm  34782  cvmsss2  35861  cvmliftmolem2  35869  cvmliftlem15  35885  cvmlift2lem9a  35890  cvmlift2lem9  35898  cvmlift2lem10  35899  cvmlift3lem6  35911  cvmlift3lem8  35913  dvtanlem  38426  resuppsinopn  43246  rfcnpre1  45861  rfcnpre2  45873  icccncfext  46723  dvsec  50697  dvcsc  50698  dvcot  50699