Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnfldtopon | Structured version Visualization version GIF version |
Description: The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
Ref | Expression |
---|---|
cnfldtopn.1 | ⊢ 𝐽 = (TopOpen‘ℂfld) |
Ref | Expression |
---|---|
cnfldtopon | ⊢ 𝐽 ∈ (TopOn‘ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfldtps 24054 | . 2 ⊢ ℂfld ∈ TopSp | |
2 | cnfldbas 20714 | . . 3 ⊢ ℂ = (Base‘ℂfld) | |
3 | cnfldtopn.1 | . . 3 ⊢ 𝐽 = (TopOpen‘ℂfld) | |
4 | 2, 3 | istps 22196 | . 2 ⊢ (ℂfld ∈ TopSp ↔ 𝐽 ∈ (TopOn‘ℂ)) |
5 | 1, 4 | mpbi 229 | 1 ⊢ 𝐽 ∈ (TopOn‘ℂ) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 ‘cfv 6491 ℂcc 10982 TopOpenctopn 17237 ℂfldccnfld 20710 TopOnctopon 22172 TopSpctps 22194 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5240 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7662 ax-cnex 11040 ax-resscn 11041 ax-1cn 11042 ax-icn 11043 ax-addcl 11044 ax-addrcl 11045 ax-mulcl 11046 ax-mulrcl 11047 ax-mulcom 11048 ax-addass 11049 ax-mulass 11050 ax-distr 11051 ax-i2m1 11052 ax-1ne0 11053 ax-1rid 11054 ax-rnegex 11055 ax-rrecex 11056 ax-cnre 11057 ax-pre-lttri 11058 ax-pre-lttrn 11059 ax-pre-ltadd 11060 ax-pre-mulgt0 11061 ax-pre-sup 11062 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4864 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5528 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5585 df-we 5587 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-pred 6249 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-riota 7305 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7793 df-1st 7911 df-2nd 7912 df-frecs 8179 df-wrecs 8210 df-recs 8284 df-rdg 8323 df-1o 8379 df-er 8581 df-map 8700 df-en 8817 df-dom 8818 df-sdom 8819 df-fin 8820 df-sup 9311 df-inf 9312 df-pnf 11124 df-mnf 11125 df-xr 11126 df-ltxr 11127 df-le 11128 df-sub 11320 df-neg 11321 df-div 11746 df-nn 12087 df-2 12149 df-3 12150 df-4 12151 df-5 12152 df-6 12153 df-7 12154 df-8 12155 df-9 12156 df-n0 12347 df-z 12433 df-dec 12551 df-uz 12696 df-q 12802 df-rp 12844 df-xneg 12961 df-xadd 12962 df-xmul 12963 df-fz 13353 df-seq 13835 df-exp 13896 df-cj 14917 df-re 14918 df-im 14919 df-sqrt 15053 df-abs 15054 df-struct 16953 df-slot 16988 df-ndx 17000 df-base 17018 df-plusg 17080 df-mulr 17081 df-starv 17082 df-tset 17086 df-ple 17087 df-ds 17089 df-unif 17090 df-rest 17238 df-topn 17239 df-topgen 17259 df-psmet 20702 df-xmet 20703 df-met 20704 df-bl 20705 df-mopn 20706 df-cnfld 20711 df-top 22156 df-topon 22173 df-topsp 22195 df-bases 22209 df-xms 23586 df-ms 23587 |
This theorem is referenced by: cnfldtop 24060 unicntop 24062 sszcld 24093 reperflem 24094 cnperf 24096 divcn 24144 fsumcn 24146 expcn 24148 divccn 24149 cncfcn1 24187 cncfmptc 24188 cncfmptid 24189 cncfmpt2f 24191 cdivcncf 24197 abscncfALT 24200 cncfcnvcn 24201 cnmptre 24203 iirevcn 24206 iihalf1cn 24208 iihalf2cn 24210 iimulcn 24214 icchmeo 24217 cnrehmeo 24229 cnheiborlem 24230 cnheibor 24231 cnllycmp 24232 evth 24235 evth2 24236 lebnumlem2 24238 reparphti 24273 pcoass 24300 mbfimaopnlem 24932 limcvallem 25148 ellimc2 25154 limcnlp 25155 limcflflem 25157 limcflf 25158 limcmo 25159 limcres 25163 cnplimc 25164 cnlimc 25165 limccnp 25168 limccnp2 25169 dvbss 25178 perfdvf 25180 recnperf 25182 dvreslem 25186 dvres2lem 25187 dvres3a 25191 dvidlem 25192 dvcnp2 25197 dvcn 25198 dvnres 25208 dvaddbr 25215 dvmulbr 25216 dvcmulf 25222 dvcobr 25223 dvcjbr 25226 dvrec 25232 dvmptid 25234 dvmptc 25235 dvmptres2 25239 dvmptcmul 25241 dvmptntr 25248 dvmptfsum 25252 dvcnvlem 25253 dvcnv 25254 dvexp3 25255 dveflem 25256 dvlipcn 25271 lhop1lem 25290 lhop2 25292 lhop 25293 dvcnvrelem2 25295 dvcnvre 25296 ftc1lem3 25315 ftc1cn 25320 plycn 25535 dvply1 25557 dvtaylp 25642 taylthlem1 25645 taylthlem2 25646 ulmdvlem3 25674 psercn2 25695 psercn 25698 pserdvlem2 25700 pserdv 25701 abelth 25713 pige3ALT 25789 logcn 25915 dvloglem 25916 dvlog 25919 dvlog2 25921 efopnlem2 25925 efopn 25926 logtayl 25928 dvcxp1 26006 cxpcn 26011 cxpcn2 26012 cxpcn3 26014 resqrtcn 26015 sqrtcn 26016 loglesqrt 26024 atansopn 26195 dvatan 26198 xrlimcnp 26231 efrlim 26232 lgamucov 26300 ftalem3 26337 vmcn 29418 dipcn 29439 ipasslem7 29555 ipasslem8 29556 occllem 30022 nlelchi 30780 tpr2rico 32227 rmulccn 32243 raddcn 32244 cxpcncf1 32942 cvxpconn 33570 cvxsconn 33571 cnllysconn 33573 sinccvglem 33996 ivthALT 34666 knoppcnlem10 34824 knoppcnlem11 34825 broucube 35971 dvtanlem 35986 dvtan 35987 ftc1cnnc 36009 dvasin 36021 dvacos 36022 dvreasin 36023 dvreacos 36024 areacirclem1 36025 areacirclem2 36026 areacirclem4 36028 refsumcn 42950 fprodcnlem 43532 fprodcn 43533 fsumcncf 43811 ioccncflimc 43818 cncfuni 43819 icocncflimc 43822 cncfdmsn 43823 cncfiooicclem1 43826 cxpcncf2 43832 fprodsub2cncf 43838 fprodadd2cncf 43839 dvmptconst 43848 dvmptidg 43850 dvresntr 43851 itgsubsticclem 43908 dirkercncflem2 44037 dirkercncflem4 44039 dirkercncf 44040 fourierdlem32 44072 fourierdlem33 44073 fourierdlem62 44101 fourierdlem93 44132 fourierdlem101 44140 |
Copyright terms: Public domain | W3C validator |