| 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 2730 | . . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
| 2 | eqid 2730 | . . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾 | |
| 3 | 1, 2 | iscn2 23132 | . . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
| 4 | 3 | simprbi 496 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
| 5 | 4 | simprd 495 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽) |
| 6 | imaeq2 6030 | . . . 4 ⊢ (𝑥 = 𝐴 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝐴)) | |
| 7 | 6 | eleq1d 2814 | . . 3 ⊢ (𝑥 = 𝐴 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ 𝐽)) |
| 8 | 7 | rspccva 3590 | . 2 ⊢ ((∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
| 9 | 5, 8 | sylan 580 | 1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∪ cuni 4874 ◡ccnv 5640 “ cima 5644 ⟶wf 6510 (class class class)co 7390 Topctop 22787 Cn ccn 23118 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3757 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-fv 6522 df-ov 7393 df-oprab 7394 df-mpo 7395 df-map 8804 df-top 22788 df-topon 22805 df-cn 23121 |
| This theorem is referenced by: cnco 23160 cnclima 23162 cnntri 23165 cnss1 23170 cnss2 23171 cncnpi 23172 cnrest 23179 cnt0 23240 cnhaus 23248 cncmp 23286 cnconn 23316 2ndcomap 23352 kgencn3 23452 txcnmpt 23518 txdis1cn 23529 pthaus 23532 ptrescn 23533 txkgen 23546 xkoco2cn 23552 xkococnlem 23553 txconn 23583 imasnopn 23584 qtopkgen 23604 qtopss 23609 isr0 23631 kqreglem1 23635 kqreglem2 23636 kqnrmlem1 23637 kqnrmlem2 23638 hmeoima 23659 hmeoopn 23660 hmeoimaf1o 23664 reghmph 23687 nrmhmph 23688 tmdgsum2 23990 symgtgp 24000 ghmcnp 24009 tgpt0 24013 qustgpopn 24014 qustgplem 24015 nmhmcn 25027 mbfimaopnlem 25563 cncombf 25566 cnmbf 25567 dvloglem 26564 efopnlem2 26573 efopn 26574 atansopn 26849 cnmbfm 34261 cvmsss2 35268 cvmliftmolem2 35276 cvmliftlem15 35292 cvmlift2lem9a 35297 cvmlift2lem9 35305 cvmlift2lem10 35306 cvmlift3lem6 35318 cvmlift3lem8 35320 dvtanlem 37670 resuppsinopn 42358 rfcnpre1 45020 rfcnpre2 45032 icccncfext 45892 |
| Copyright terms: Public domain | W3C validator |