![]() |
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 2771 | . . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | eqid 2771 | . . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾 | |
3 | 1, 2 | iscn2 21565 | . . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 489 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simprd 488 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽) |
6 | imaeq2 5763 | . . . 4 ⊢ (𝑥 = 𝐴 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝐴)) | |
7 | 6 | eleq1d 2843 | . . 3 ⊢ (𝑥 = 𝐴 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ 𝐽)) |
8 | 7 | rspccva 3527 | . 2 ⊢ ((∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
9 | 5, 8 | sylan 572 | 1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1508 ∈ wcel 2051 ∀wral 3081 ∪ cuni 4708 ◡ccnv 5402 “ cima 5406 ⟶wf 6181 (class class class)co 6974 Topctop 21220 Cn ccn 21551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ral 3086 df-rex 3087 df-rab 3090 df-v 3410 df-sbc 3675 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-fv 6193 df-ov 6977 df-oprab 6978 df-mpo 6979 df-map 8206 df-top 21221 df-topon 21238 df-cn 21554 |
This theorem is referenced by: cnco 21593 cnclima 21595 cnntri 21598 cnss1 21603 cnss2 21604 cncnpi 21605 cnrest 21612 cnt0 21673 cnhaus 21681 cncmp 21719 cnconn 21749 2ndcomap 21785 kgencn3 21885 txcnmpt 21951 txdis1cn 21962 pthaus 21965 ptrescn 21966 txkgen 21979 xkoco2cn 21985 xkococnlem 21986 txconn 22016 imasnopn 22017 qtopkgen 22037 qtopss 22042 isr0 22064 kqreglem1 22068 kqreglem2 22069 kqnrmlem1 22070 kqnrmlem2 22071 hmeoima 22092 hmeoopn 22093 hmeoimaf1o 22097 reghmph 22120 nrmhmph 22121 tmdgsum2 22423 symgtgp 22428 ghmcnp 22441 tgpt0 22445 qustgpopn 22446 qustgplem 22447 nmhmcn 23442 mbfimaopnlem 23974 cncombf 23977 cnmbf 23978 dvloglem 24947 efopnlem2 24956 efopn 24957 atansopn 25226 cnmbfm 31198 cvmsss2 32143 cvmliftmolem2 32151 cvmliftlem15 32167 cvmlift2lem9a 32172 cvmlift2lem9 32180 cvmlift2lem10 32181 cvmlift3lem6 32193 cvmlift3lem8 32195 dvtanlem 34419 rfcnpre1 40732 rfcnpre2 40744 icccncfext 41632 |
Copyright terms: Public domain | W3C validator |