![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnfldtopon | Structured version Visualization version Unicode version |
Description: The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
Ref | Expression |
---|---|
cnfldtopn.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cnfldtopon |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfldtps 21798 |
. 2
![]() ![]() ![]() | |
2 | cnfldbas 18974 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | cnfldtopn.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | istps 19951 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbi 212 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-inf 7957 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-fz 11785 df-seq 12214 df-exp 12273 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-plusg 15203 df-mulr 15204 df-starv 15205 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-rest 15321 df-topn 15322 df-topgen 15342 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-xms 21335 df-ms 21336 |
This theorem is referenced by: cnfldtop 21804 sszcld 21835 reperflem 21836 cnperf 21838 divcn 21900 fsumcn 21902 expcn 21904 divccn 21905 cncfcn1 21942 cncfmptc 21943 cncfmptid 21944 cncfmpt2f 21946 cdivcncf 21949 abscncfALT 21952 cncfcnvcn 21953 cnmptre 21955 iirevcn 21958 iihalf1cn 21960 iihalf2cn 21962 iimulcn 21966 icchmeo 21969 cnrehmeo 21981 cnheiborlem 21982 cnheibor 21983 cnllycmp 21984 evth 21987 evth2 21988 lebnumlem2 21990 lebnumlem2OLD 21993 reparphti 22028 pcoass 22055 csscld 22220 clsocv 22221 cncmet 22290 resscdrg 22325 mbfimaopnlem 22611 limcvallem 22826 ellimc2 22832 limcnlp 22833 limcflflem 22835 limcflf 22836 limcmo 22837 limcres 22841 cnplimc 22842 cnlimc 22843 limccnp 22846 limccnp2 22847 limciun 22849 dvbss 22856 perfdvf 22858 recnperf 22860 dvreslem 22864 dvres2lem 22865 dvres3a 22869 dvidlem 22870 dvcnp2 22874 dvcn 22875 dvnres 22885 dvaddbr 22892 dvmulbr 22893 dvcmulf 22899 dvcobr 22900 dvcjbr 22903 dvrec 22909 dvmptid 22911 dvmptc 22912 dvmptres2 22916 dvmptcmul 22918 dvmptntr 22925 dvmptfsum 22927 dvcnvlem 22928 dvcnv 22929 dvexp3 22930 dveflem 22931 dvlipcn 22946 lhop1lem 22965 lhop2 22967 lhop 22968 dvcnvrelem2 22970 dvcnvre 22971 ftc1lem3 22990 ftc1cn 22995 plycn 23215 dvply1 23237 dvtaylp 23325 taylthlem1 23328 taylthlem2 23329 ulmdvlem3 23357 psercn2 23378 psercn 23381 pserdvlem2 23383 pserdv 23384 abelth 23396 pige3 23472 logcn 23592 dvloglem 23593 logdmopn 23594 dvlog 23596 dvlog2 23598 efopnlem2 23602 efopn 23603 logtayl 23605 dvcxp1 23680 cxpcn 23685 cxpcn2 23686 cxpcn3 23688 resqrtcn 23689 sqrtcn 23690 loglesqrt 23698 atansopn 23858 dvatan 23861 xrlimcnp 23894 efrlim 23895 lgamucov 23963 lgamucov2 23964 ftalem3 23999 vmcn 26335 dipcn 26359 ipasslem7 26477 ipasslem8 26478 occllem 26956 nlelchi 27714 tpr2rico 28718 rmulccn 28734 raddcn 28735 cvxpcon 29965 cvxscon 29966 cnllyscon 29968 sinccvglem 30316 ivthALT 30991 broucube 31974 dvtanlem 31990 dvtanlemOLD 31991 dvtan 31992 ftc1cnnc 32016 dvasin 32028 dvacos 32029 dvreasin 32030 dvreacos 32031 areacirclem1 32032 areacirclem2 32033 areacirclem4 32035 refsumcn 37351 unicntop 37371 fsumcncf 37755 ioccncflimc 37763 cncfuni 37764 icocncflimc 37767 cncfdmsn 37768 cncfiooicclem1 37771 cxpcncf2 37778 dvmptconst 37785 dvmptidg 37787 dvresntr 37788 itgsubsticclem 37852 dirkercncflem2 37966 dirkercncflem4 37968 dirkercncf 37969 fourierdlem32 38002 fourierdlem33 38003 fourierdlem62 38032 fourierdlem93 38063 fourierdlem101 38071 |
Copyright terms: Public domain | W3C validator |