Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnima | Structured version Visualization version GIF version |
Description: An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.) |
Ref | Expression |
---|---|
cnima | ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2818 | . . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | eqid 2818 | . . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾 | |
3 | 1, 2 | iscn2 21774 | . . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 497 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simprd 496 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽) |
6 | imaeq2 5918 | . . . 4 ⊢ (𝑥 = 𝐴 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝐴)) | |
7 | 6 | eleq1d 2894 | . . 3 ⊢ (𝑥 = 𝐴 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ 𝐽)) |
8 | 7 | rspccva 3619 | . 2 ⊢ ((∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
9 | 5, 8 | sylan 580 | 1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∀wral 3135 ∪ cuni 4830 ◡ccnv 5547 “ cima 5551 ⟶wf 6344 (class class class)co 7145 Topctop 21429 Cn ccn 21760 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-fv 6356 df-ov 7148 df-oprab 7149 df-mpo 7150 df-map 8397 df-top 21430 df-topon 21447 df-cn 21763 |
This theorem is referenced by: cnco 21802 cnclima 21804 cnntri 21807 cnss1 21812 cnss2 21813 cncnpi 21814 cnrest 21821 cnt0 21882 cnhaus 21890 cncmp 21928 cnconn 21958 2ndcomap 21994 kgencn3 22094 txcnmpt 22160 txdis1cn 22171 pthaus 22174 ptrescn 22175 txkgen 22188 xkoco2cn 22194 xkococnlem 22195 txconn 22225 imasnopn 22226 qtopkgen 22246 qtopss 22251 isr0 22273 kqreglem1 22277 kqreglem2 22278 kqnrmlem1 22279 kqnrmlem2 22280 hmeoima 22301 hmeoopn 22302 hmeoimaf1o 22306 reghmph 22329 nrmhmph 22330 tmdgsum2 22632 symgtgp 22637 ghmcnp 22650 tgpt0 22654 qustgpopn 22655 qustgplem 22656 nmhmcn 23651 mbfimaopnlem 24183 cncombf 24186 cnmbf 24187 dvloglem 25158 efopnlem2 25167 efopn 25168 atansopn 25437 cnmbfm 31420 cvmsss2 32418 cvmliftmolem2 32426 cvmliftlem15 32442 cvmlift2lem9a 32447 cvmlift2lem9 32455 cvmlift2lem10 32456 cvmlift3lem6 32468 cvmlift3lem8 32470 dvtanlem 34822 rfcnpre1 41153 rfcnpre2 41165 icccncfext 42046 |
Copyright terms: Public domain | W3C validator |