MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfldtopon Structured version   Visualization version   GIF version

Theorem cnfldtopon 23711
Description: The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypothesis
Ref Expression
cnfldtopn.1 𝐽 = (TopOpen‘ℂfld)
Assertion
Ref Expression
cnfldtopon 𝐽 ∈ (TopOn‘ℂ)

Proof of Theorem cnfldtopon
StepHypRef Expression
1 cnfldtps 23706 . 2 fld ∈ TopSp
2 cnfldbas 20399 . . 3 ℂ = (Base‘ℂfld)
3 cnfldtopn.1 . . 3 𝐽 = (TopOpen‘ℂfld)
42, 3istps 21862 . 2 (ℂfld ∈ TopSp ↔ 𝐽 ∈ (TopOn‘ℂ))
51, 4mpbi 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