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 23706 | . 2 ⊢ ℂfld ∈ TopSp | |
2 | cnfldbas 20399 | . . 3 ⊢ ℂ = (Base‘ℂfld) | |
3 | cnfldtopn.1 | . . 3 ⊢ 𝐽 = (TopOpen‘ℂfld) | |
4 | 2, 3 | istps 21862 | . 2 ⊢ (ℂfld ∈ TopSp ↔ 𝐽 ∈ (TopOn‘ℂ)) |
5 | 1, 4 | mpbi 233 | 1 ⊢ 𝐽 ∈ (TopOn‘ℂ) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2112 ‘cfv 6400 ℂcc 10756 TopOpenctopn 16958 ℂfldccnfld 20395 TopOnctopon 21838 TopSpctps 21860 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5195 ax-sep 5208 ax-nul 5215 ax-pow 5274 ax-pr 5338 ax-un 7544 ax-cnex 10814 ax-resscn 10815 ax-1cn 10816 ax-icn 10817 ax-addcl 10818 ax-addrcl 10819 ax-mulcl 10820 ax-mulrcl 10821 ax-mulcom 10822 ax-addass 10823 ax-mulass 10824 ax-distr 10825 ax-i2m1 10826 ax-1ne0 10827 ax-1rid 10828 ax-rnegex 10829 ax-rrecex 10830 ax-cnre 10831 ax-pre-lttri 10832 ax-pre-lttrn 10833 ax-pre-ltadd 10834 ax-pre-mulgt0 10835 ax-pre-sup 10836 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4456 df-pw 4531 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4836 df-iun 4922 df-br 5070 df-opab 5132 df-mpt 5152 df-tr 5178 df-id 5471 df-eprel 5477 df-po 5485 df-so 5486 df-fr 5526 df-we 5528 df-xp 5574 df-rel 5575 df-cnv 5576 df-co 5577 df-dm 5578 df-rn 5579 df-res 5580 df-ima 5581 df-pred 6178 df-ord 6236 df-on 6237 df-lim 6238 df-suc 6239 df-iota 6358 df-fun 6402 df-fn 6403 df-f 6404 df-f1 6405 df-fo 6406 df-f1o 6407 df-fv 6408 df-riota 7191 df-ov 7237 df-oprab 7238 df-mpo 7239 df-om 7666 df-1st 7782 df-2nd 7783 df-wrecs 8070 df-recs 8131 df-rdg 8169 df-1o 8225 df-er 8414 df-map 8533 df-en 8650 df-dom 8651 df-sdom 8652 df-fin 8653 df-sup 9087 df-inf 9088 df-pnf 10898 df-mnf 10899 df-xr 10900 df-ltxr 10901 df-le 10902 df-sub 11093 df-neg 11094 df-div 11519 df-nn 11860 df-2 11922 df-3 11923 df-4 11924 df-5 11925 df-6 11926 df-7 11927 df-8 11928 df-9 11929 df-n0 12120 df-z 12206 df-dec 12323 df-uz 12468 df-q 12574 df-rp 12616 df-xneg 12733 df-xadd 12734 df-xmul 12735 df-fz 13125 df-seq 13606 df-exp 13667 df-cj 14694 df-re 14695 df-im 14696 df-sqrt 14830 df-abs 14831 df-struct 16732 df-slot 16767 df-ndx 16777 df-base 16793 df-plusg 16847 df-mulr 16848 df-starv 16849 df-tset 16853 df-ple 16854 df-ds 16856 df-unif 16857 df-rest 16959 df-topn 16960 df-topgen 16980 df-psmet 20387 df-xmet 20388 df-met 20389 df-bl 20390 df-mopn 20391 df-cnfld 20396 df-top 21822 df-topon 21839 df-topsp 21861 df-bases 21874 df-xms 23249 df-ms 23250 |
This theorem is referenced by: cnfldtop 23712 unicntop 23714 sszcld 23745 reperflem 23746 cnperf 23748 divcn 23796 fsumcn 23798 expcn 23800 divccn 23801 cncfcn1 23839 cncfmptc 23840 cncfmptid 23841 cncfmpt2f 23843 cdivcncf 23849 abscncfALT 23852 cncfcnvcn 23853 cnmptre 23855 iirevcn 23858 iihalf1cn 23860 iihalf2cn 23862 iimulcn 23866 icchmeo 23869 cnrehmeo 23881 cnheiborlem 23882 cnheibor 23883 cnllycmp 23884 evth 23887 evth2 23888 lebnumlem2 23890 reparphti 23925 pcoass 23952 mbfimaopnlem 24583 limcvallem 24799 ellimc2 24805 limcnlp 24806 limcflflem 24808 limcflf 24809 limcmo 24810 limcres 24814 cnplimc 24815 cnlimc 24816 limccnp 24819 limccnp2 24820 dvbss 24829 perfdvf 24831 recnperf 24833 dvreslem 24837 dvres2lem 24838 dvres3a 24842 dvidlem 24843 dvcnp2 24848 dvcn 24849 dvnres 24859 dvaddbr 24866 dvmulbr 24867 dvcmulf 24873 dvcobr 24874 dvcjbr 24877 dvrec 24883 dvmptid 24885 dvmptc 24886 dvmptres2 24890 dvmptcmul 24892 dvmptntr 24899 dvmptfsum 24903 dvcnvlem 24904 dvcnv 24905 dvexp3 24906 dveflem 24907 dvlipcn 24922 lhop1lem 24941 lhop2 24943 lhop 24944 dvcnvrelem2 24946 dvcnvre 24947 ftc1lem3 24966 ftc1cn 24971 plycn 25186 dvply1 25208 dvtaylp 25293 taylthlem1 25296 taylthlem2 25297 ulmdvlem3 25325 psercn2 25346 psercn 25349 pserdvlem2 25351 pserdv 25352 abelth 25364 pige3ALT 25440 logcn 25566 dvloglem 25567 dvlog 25570 dvlog2 25572 efopnlem2 25576 efopn 25577 logtayl 25579 dvcxp1 25657 cxpcn 25662 cxpcn2 25663 cxpcn3 25665 resqrtcn 25666 sqrtcn 25667 loglesqrt 25675 atansopn 25846 dvatan 25849 xrlimcnp 25882 efrlim 25883 lgamucov 25951 ftalem3 25988 vmcn 28811 dipcn 28832 ipasslem7 28948 ipasslem8 28949 occllem 29415 nlelchi 30173 tpr2rico 31607 rmulccn 31623 raddcn 31624 cxpcncf1 32318 cvxpconn 32947 cvxsconn 32948 cnllysconn 32950 sinccvglem 33373 ivthALT 34294 knoppcnlem10 34452 knoppcnlem11 34453 broucube 35584 dvtanlem 35599 dvtan 35600 ftc1cnnc 35622 dvasin 35634 dvacos 35635 dvreasin 35636 dvreacos 35637 areacirclem1 35638 areacirclem2 35639 areacirclem4 35641 refsumcn 42293 fprodcnlem 42860 fprodcn 42861 fsumcncf 43139 ioccncflimc 43146 cncfuni 43147 icocncflimc 43150 cncfdmsn 43151 cncfiooicclem1 43154 cxpcncf2 43160 fprodsub2cncf 43166 fprodadd2cncf 43167 dvmptconst 43176 dvmptidg 43178 dvresntr 43179 itgsubsticclem 43236 dirkercncflem2 43365 dirkercncflem4 43367 dirkercncf 43368 fourierdlem32 43400 fourierdlem33 43401 fourierdlem62 43429 fourierdlem93 43460 fourierdlem101 43468 |
Copyright terms: Public domain | W3C validator |