Theorem cnfldtopon 22956

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

Step	Hyp	Ref	Expression
1		cnfldtps 22951	. 2 ⊢ ℂfld ∈ TopSp
2		cnfldbas 20110	. . 3 ⊢ ℂ = (Base‘ℂfld)
3		cnfldtopn.1	. . 3 ⊢ 𝐽 = (TopOpen‘ℂfld)
4	2, 3	istps 21109	. 2 ⊢ (ℂfld ∈ TopSp ↔ 𝐽 ∈ (TopOn‘ℂ))
5	1, 4	mpbi 222	1 ⊢ 𝐽 ∈ (TopOn‘ℂ)

Syntax hints:   = wceq 1658   ∈ wcel 2166  ‘cfv 6123  ℂcc 10250  TopOpenctopn 16435  ℂ_fldccnfld 20106  TopOnctopon 21085  TopSpctps 21107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-inf 8618  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-q 12072  df-rp 12113  df-xneg 12232  df-xadd 12233  df-xmul 12234  df-fz 12620  df-seq 13096  df-exp 13155  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-plusg 16318  df-mulr 16319  df-starv 16320  df-tset 16324  df-ple 16325  df-ds 16327  df-unif 16328  df-rest 16436  df-topn 16437  df-topgen 16457  df-psmet 20098  df-xmet 20099  df-met 20100  df-bl 20101  df-mopn 20102  df-cnfld 20107  df-top 21069  df-topon 21086  df-topsp 21108  df-bases 21121  df-xms 22495  df-ms 22496

This theorem is referenced by:  cnfldtop  22957  unicntop  22959  sszcld  22990  reperflem  22991  cnperf  22993  divcn  23041  fsumcn  23043  expcn  23045  divccn  23046  cncfcn1  23083  cncfmptc  23084  cncfmptid  23085  cncfmpt2f  23087  cdivcncf  23090  abscncfALT  23093  cncfcnvcn  23094  cnmptre  23096  iirevcn  23099  iihalf1cn  23101  iihalf2cn  23103  iimulcn  23107  icchmeo  23110  cnrehmeo  23122  cnheiborlem  23123  cnheibor  23124  cnllycmp  23125  evth  23128  evth2  23129  lebnumlem2  23131  reparphti  23166  pcoass  23193  csscld  23417  clsocv  23418  cncmet  23490  resscdrg  23526  mbfimaopnlem  23821  limcvallem  24034  ellimc2  24040  limcnlp  24041  limcflflem  24043  limcflf  24044  limcmo  24045  limcres  24049  cnplimc  24050  cnlimc  24051  limccnp  24054  limccnp2  24055  limciun  24057  dvbss  24064  perfdvf  24066  recnperf  24068  dvreslem  24072  dvres2lem  24073  dvres3a  24077  dvidlem  24078  dvcnp2  24082  dvcn  24083  dvnres  24093  dvaddbr  24100  dvmulbr  24101  dvcmulf  24107  dvcobr  24108  dvcjbr  24111  dvrec  24117  dvmptid  24119  dvmptc  24120  dvmptres2  24124  dvmptcmul  24126  dvmptntr  24133  dvmptfsum  24137  dvcnvlem  24138  dvcnv  24139  dvexp3  24140  dveflem  24141  dvlipcn  24156  lhop1lem  24175  lhop2  24177  lhop  24178  dvcnvrelem2  24180  dvcnvre  24181  ftc1lem3  24200  ftc1cn  24205  plycn  24416  dvply1  24438  dvtaylp  24523  taylthlem1  24526  taylthlem2  24527  ulmdvlem3  24555  psercn2  24576  psercn  24579  pserdvlem2  24581  pserdv  24582  abelth  24594  pige3  24669  logcn  24792  dvloglem  24793  logdmopn  24794  dvlog  24796  dvlog2  24798  efopnlem2  24802  efopn  24803  logtayl  24805  dvcxp1  24883  cxpcn  24888  cxpcn2  24889  cxpcn3  24891  resqrtcn  24892  sqrtcn  24893  loglesqrt  24901  atansopn  25072  dvatan  25075  xrlimcnp  25108  efrlim  25109  lgamucov  25177  lgamucov2  25178  ftalem3  25214  vmcn  28109  dipcn  28130  ipasslem7  28246  ipasslem8  28247  occllem  28717  nlelchi  29475  tpr2rico  30503  rmulccn  30519  raddcn  30520  cxpcncf1  31222  cvxpconn  31770  cvxsconn  31771  cnllysconn  31773  sinccvglem  32110  ivthALT  32868  knoppcnlem10  33025  knoppcnlem11  33026  broucube  33987  dvtanlem  34002  dvtan  34003  ftc1cnnc  34027  dvasin  34039  dvacos  34040  dvreasin  34041  dvreacos  34042  areacirclem1  34043  areacirclem2  34044  areacirclem4  34046  refsumcn  40007  fprodcnlem  40626  fprodcn  40627  fsumcncf  40886  ioccncflimc  40893  cncfuni  40894  icocncflimc  40897  cncfdmsn  40898  cncfiooicclem1  40901  cxpcncf2  40908  fprodsub2cncf  40914  fprodadd2cncf  40915  dvmptconst  40924  dvmptidg  40926  dvresntr  40927  itgsubsticclem  40985  dirkercncflem2  41115  dirkercncflem4  41117  dirkercncf  41118  fourierdlem32  41150  fourierdlem33  41151  fourierdlem62  41179  fourierdlem93  41210  fourierdlem101  41218