Theorem cnima 23156

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ∀wral 3056  ∪ cuni 4903  ^◡ccnv 5671   “ cima 5675  ⟶wf 6538  (class class class)co 7414  Topctop 22782   Cn ccn 23115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-map 8838  df-top 22783  df-topon 22800  df-cn 23118

This theorem is referenced by:  cnco  23157  cnclima  23159  cnntri  23162  cnss1  23167  cnss2  23168  cncnpi  23169  cnrest  23176  cnt0  23237  cnhaus  23245  cncmp  23283  cnconn  23313  2ndcomap  23349  kgencn3  23449  txcnmpt  23515  txdis1cn  23526  pthaus  23529  ptrescn  23530  txkgen  23543  xkoco2cn  23549  xkococnlem  23550  txconn  23580  imasnopn  23581  qtopkgen  23601  qtopss  23606  isr0  23628  kqreglem1  23632  kqreglem2  23633  kqnrmlem1  23634  kqnrmlem2  23635  hmeoima  23656  hmeoopn  23657  hmeoimaf1o  23661  reghmph  23684  nrmhmph  23685  tmdgsum2  23987  symgtgp  23997  ghmcnp  24006  tgpt0  24010  qustgpopn  24011  qustgplem  24012  nmhmcn  25034  mbfimaopnlem  25571  cncombf  25574  cnmbf  25575  dvloglem  26569  efopnlem2  26578  efopn  26579  atansopn  26851  cnmbfm  33819  cvmsss2  34820  cvmliftmolem2  34828  cvmliftlem15  34844  cvmlift2lem9a  34849  cvmlift2lem9  34857  cvmlift2lem10  34858  cvmlift3lem6  34870  cvmlift3lem8  34872  dvtanlem  37077  rfcnpre1  44304  rfcnpre2  44316  icccncfext  45198