![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cntop2 | Structured version Visualization version GIF version |
Description: Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
cntop2 | ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2825 | . . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | eqid 2825 | . . . 4 ⊢ ∪ 𝐾 = ∪ 𝐾 | |
3 | 1, 2 | iscn2 21413 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simplbi 493 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) |
5 | 4 | simprd 491 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2166 ∀wral 3117 ∪ cuni 4658 ◡ccnv 5341 “ cima 5345 ⟶wf 6119 (class class class)co 6905 Topctop 21068 Cn ccn 21399 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pow 5065 ax-pr 5127 ax-un 7209 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-mpt 4953 df-id 5250 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 df-iota 6086 df-fun 6125 df-fn 6126 df-f 6127 df-fv 6131 df-ov 6908 df-oprab 6909 df-mpt2 6910 df-map 8124 df-top 21069 df-topon 21086 df-cn 21402 |
This theorem is referenced by: cnco 21441 cncls2i 21445 cnntri 21446 cnss1 21451 cncnpi 21453 cncnp2 21456 cnrest 21460 cnrest2r 21462 paste 21469 cncmp 21566 rncmp 21570 cnconn 21596 connima 21599 conncn 21600 2ndcomap 21632 kgen2cn 21733 txcnmpt 21798 uptx 21799 lmcn2 21823 xkoco1cn 21831 xkoco2cn 21832 xkococnlem 21833 cnmpt11 21837 cnmpt11f 21838 cnmpt1t 21839 cnmpt12 21841 cnmpt21 21845 cnmpt2t 21847 cnmpt22 21848 cnmpt22f 21849 cnmptcom 21852 cnmpt2k 21862 qtopeu 21890 hmeofval 21932 hmeof1o 21938 hmeontr 21943 hmeores 21945 hmeoqtop 21949 hmphen 21959 reghmph 21967 nrmhmph 21968 txhmeo 21977 xpstopnlem1 21983 flfcntr 22217 cnmpt2pc 23097 ishtpy 23141 htpyco1 23147 htpyco2 23148 isphtpy 23150 phtpyco2 23159 isphtpc 23163 pcofval 23179 pcopt 23191 pcopt2 23192 pcorevlem 23195 pi1cof 23228 pi1coghm 23230 cnmbfm 30870 cnpconn 31758 |
Copyright terms: Public domain | W3C validator |