Theorem cnima 23188

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ∪ cuni 4880  ^◡ccnv 5650   “ cima 5654  ⟶wf 6523  (class class class)co 7399  Topctop 22816   Cn ccn 23147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-ov 7402  df-oprab 7403  df-mpo 7404  df-map 8836  df-top 22817  df-topon 22834  df-cn 23150

This theorem is referenced by:  cnco  23189  cnclima  23191  cnntri  23194  cnss1  23199  cnss2  23200  cncnpi  23201  cnrest  23208  cnt0  23269  cnhaus  23277  cncmp  23315  cnconn  23345  2ndcomap  23381  kgencn3  23481  txcnmpt  23547  txdis1cn  23558  pthaus  23561  ptrescn  23562  txkgen  23575  xkoco2cn  23581  xkococnlem  23582  txconn  23612  imasnopn  23613  qtopkgen  23633  qtopss  23638  isr0  23660  kqreglem1  23664  kqreglem2  23665  kqnrmlem1  23666  kqnrmlem2  23667  hmeoima  23688  hmeoopn  23689  hmeoimaf1o  23693  reghmph  23716  nrmhmph  23717  tmdgsum2  24019  symgtgp  24029  ghmcnp  24038  tgpt0  24042  qustgpopn  24043  qustgplem  24044  nmhmcn  25056  mbfimaopnlem  25593  cncombf  25596  cnmbf  25597  dvloglem  26593  efopnlem2  26602  efopn  26603  atansopn  26878  cnmbfm  34203  cvmsss2  35217  cvmliftmolem2  35225  cvmliftlem15  35241  cvmlift2lem9a  35246  cvmlift2lem9  35254  cvmlift2lem10  35255  cvmlift3lem6  35267  cvmlift3lem8  35269  dvtanlem  37614  resuppsinopn  42331  rfcnpre1  44970  rfcnpre2  44982  icccncfext  45846