![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > cnfldtopon | Structured 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 20492 |
. 2
![]() ![]() ![]() | |
2 | cnfldbas 17950 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | cnfldtopn.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | istps 18676 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbi 208 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4514 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485 ax-cnex 9452 ax-resscn 9453 ax-1cn 9454 ax-icn 9455 ax-addcl 9456 ax-addrcl 9457 ax-mulcl 9458 ax-mulrcl 9459 ax-mulcom 9460 ax-addass 9461 ax-mulass 9462 ax-distr 9463 ax-i2m1 9464 ax-1ne0 9465 ax-1rid 9466 ax-rnegex 9467 ax-rrecex 9468 ax-cnre 9469 ax-pre-lttri 9470 ax-pre-lttrn 9471 ax-pre-ltadd 9472 ax-pre-mulgt0 9473 ax-pre-sup 9474 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rmo 2807 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-int 4240 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-om 6590 df-1st 6690 df-2nd 6691 df-recs 6945 df-rdg 6979 df-1o 7033 df-oadd 7037 df-er 7214 df-map 7329 df-en 7424 df-dom 7425 df-sdom 7426 df-fin 7427 df-sup 7805 df-pnf 9534 df-mnf 9535 df-xr 9536 df-ltxr 9537 df-le 9538 df-sub 9711 df-neg 9712 df-div 10108 df-nn 10437 df-2 10494 df-3 10495 df-4 10496 df-5 10497 df-6 10498 df-7 10499 df-8 10500 df-9 10501 df-10 10502 df-n0 10694 df-z 10761 df-dec 10870 df-uz 10976 df-q 11068 df-rp 11106 df-xneg 11203 df-xadd 11204 df-xmul 11205 df-fz 11558 df-seq 11927 df-exp 11986 df-cj 12709 df-re 12710 df-im 12711 df-sqr 12845 df-abs 12846 df-struct 14297 df-ndx 14298 df-slot 14299 df-base 14300 df-plusg 14373 df-mulr 14374 df-starv 14375 df-tset 14379 df-ple 14380 df-ds 14382 df-unif 14383 df-rest 14483 df-topn 14484 df-topgen 14504 df-psmet 17937 df-xmet 17938 df-met 17939 df-bl 17940 df-mopn 17941 df-cnfld 17947 df-top 18638 df-bases 18640 df-topon 18641 df-topsp 18642 df-xms 20030 df-ms 20031 |
This theorem is referenced by: cnfldtop 20498 sszcld 20529 reperflem 20530 cnperf 20532 divcn 20579 fsumcn 20581 expcn 20583 divccn 20584 cncfcn1 20621 cncfmptc 20622 cncfmptid 20623 cncfmpt2f 20625 cdivcncf 20628 abscncfALT 20631 cncfcnvcn 20632 cnmptre 20634 iirevcn 20637 iihalf1cn 20639 iihalf2cn 20641 iimulcn 20645 icchmeo 20648 cnrehmeo 20660 cnheiborlem 20661 cnheibor 20662 cnllycmp 20663 evth 20666 evth2 20667 lebnumlem2 20669 reparphti 20704 pcoass 20731 csscld 20896 clsocv 20897 cncmet 20968 resscdrg 21005 mbfimaopnlem 21269 limcvallem 21482 ellimc2 21488 limcnlp 21489 limcflflem 21491 limcflf 21492 limcmo 21493 limcres 21497 cnplimc 21498 cnlimc 21499 limccnp 21502 limccnp2 21503 limciun 21505 dvbss 21512 perfdvf 21514 recnperf 21516 dvreslem 21520 dvres2lem 21521 dvres3a 21525 dvidlem 21526 dvcnp2 21530 dvcn 21531 dvnres 21541 dvaddbr 21548 dvmulbr 21549 dvcmulf 21555 dvcobr 21556 dvcjbr 21559 dvrec 21565 dvmptid 21567 dvmptc 21568 dvmptres2 21572 dvmptcmul 21574 dvmptntr 21581 dvmptfsum 21583 dvcnvlem 21584 dvcnv 21585 dvexp3 21586 dveflem 21587 dvlipcn 21602 lhop1lem 21621 lhop2 21623 lhop 21624 dvcnvrelem2 21626 dvcnvre 21627 ftc1lem3 21646 ftc1cn 21651 plycn 21864 dvply1 21886 dvtaylp 21971 taylthlem1 21974 taylthlem2 21975 ulmdvlem3 22003 psercn2 22024 psercn 22027 pserdvlem2 22029 pserdv 22030 abelth 22042 pige3 22115 logcn 22228 dvloglem 22229 logdmopn 22230 dvlog 22232 dvlog2 22234 efopnlem2 22238 efopn 22239 logtayl 22241 dvcxp1 22316 cxpcn 22319 cxpcn2 22320 cxpcn3 22322 resqrcn 22323 sqrcn 22324 loglesqr 22332 atansopn 22463 dvatan 22466 xrlimcnp 22498 efrlim 22499 ftalem3 22548 vmcn 24266 dipcn 24290 ipasslem7 24408 ipasslem8 24409 occllem 24878 nlelchi 25637 tpr2rico 26507 rmulccn 26523 raddcn 26524 lgamucov 27188 lgamucov2 27189 cvxpcon 27295 cvxscon 27296 cnllyscon 27298 sinccvglem 27481 dvtanlem 28609 dvtan 28610 ftc1cnnc 28634 dvasin 28648 dvacos 28649 dvreasin 28650 dvreacos 28651 areacirclem1 28652 areacirclem2 28653 areacirclem4 28655 ivthALT 28698 refsumcn 29920 |
Copyright terms: Public domain | W3C validator |