Theorem cnfldtopon 24730

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 24725	. 2 ⊢ ℂfld ∈ TopSp
2		cnfldbas 21317	. . 3 ⊢ ℂ = (Base‘ℂfld)
3		cnfldtopn.1	. . 3 ⊢ 𝐽 = (TopOpen‘ℂfld)
4	2, 3	istps 22882	. 2 ⊢ (ℂfld ∈ TopSp ↔ 𝐽 ∈ (TopOn‘ℂ))
5	1, 4	mpbi 230	1 ⊢ 𝐽 ∈ (TopOn‘ℂ)

Syntax hints:   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  ℂcc 11028  TopOpenctopn 17345  ℂ_fldccnfld 21313  TopOnctopon 22858  TopSpctps 22880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107  ax-pre-sup 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-sup 9349  df-inf 9350  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12150  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-6 12216  df-7 12217  df-8 12218  df-9 12219  df-n0 12406  df-z 12493  df-dec 12612  df-uz 12756  df-q 12866  df-rp 12910  df-xneg 13030  df-xadd 13031  df-xmul 13032  df-fz 13428  df-seq 13929  df-exp 13989  df-cj 15026  df-re 15027  df-im 15028  df-sqrt 15162  df-abs 15163  df-struct 17078  df-slot 17113  df-ndx 17125  df-base 17141  df-plusg 17194  df-mulr 17195  df-starv 17196  df-tset 17200  df-ple 17201  df-ds 17203  df-unif 17204  df-rest 17346  df-topn 17347  df-topgen 17367  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-cnfld 21314  df-top 22842  df-topon 22859  df-topsp 22881  df-bases 22894  df-xms 24268  df-ms 24269

This theorem is referenced by:  cnfldtop  24731  unicntop  24733  sszcld  24766  reperflem  24767  cnperf  24769  divcnOLD  24817  divcn  24819  fsumcn  24821  expcn  24823  divccn  24824  expcnOLD  24825  divccnOLD  24826  cncfcn1  24864  cncfmptc  24865  cncfmptid  24866  cncfmpt2f  24868  cdivcncf  24874  abscncfALT  24878  cncfcnvcn  24879  cnmptre  24881  iirevcn  24884  iihalf1cn  24886  iihalf1cnOLD  24887  iihalf2cn  24889  iihalf2cnOLD  24890  iimulcn  24894  iimulcnOLD  24895  icchmeo  24898  icchmeoOLD  24899  cnrehmeo  24911  cnrehmeoOLD  24912  cnheiborlem  24913  cnheibor  24914  cnllycmp  24915  evth  24918  evth2  24919  lebnumlem2  24921  reparphti  24956  reparphtiOLD  24957  pcoass  24984  mulcncf  25406  mbfimaopnlem  25616  limcvallem  25832  ellimc2  25838  limcnlp  25839  limcflflem  25841  limcflf  25842  limcmo  25843  limcres  25847  cnplimc  25848  cnlimc  25849  limccnp  25852  limccnp2  25853  dvbss  25862  perfdvf  25864  recnperf  25866  dvreslem  25870  dvres2lem  25871  dvres3a  25875  dvidlem  25876  dvcnp2  25881  dvcnp2OLD  25882  dvcn  25883  dvnres  25893  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcmulf  25908  dvcobr  25909  dvcobrOLD  25910  dvcjbr  25913  dvrec  25919  dvmptid  25921  dvmptc  25922  dvmptres2  25926  dvmptcmul  25928  dvmptntr  25935  dvmptfsum  25939  dvcnvlem  25940  dvcnv  25941  dvexp3  25942  dveflem  25943  dvlipcn  25959  lhop1lem  25978  lhop2  25980  lhop  25981  dvcnvrelem2  25983  dvcnvre  25984  ftc1lem3  26005  ftc1cn  26010  plycn  26226  plycnOLD  26227  dvply1  26251  dvtaylp  26338  taylthlem1  26341  taylthlem2  26342  taylthlem2OLD  26343  ulmdvlem3  26371  psercn2  26392  psercn2OLD  26393  psercn  26396  pserdvlem2  26398  pserdv  26399  abelth  26411  pige3ALT  26489  logcn  26616  dvloglem  26617  dvlog  26620  dvlog2  26622  efopnlem2  26626  efopn  26627  logtayl  26629  dvcxp1  26709  cxpcn  26714  cxpcnOLD  26715  cxpcn2  26716  cxpcn3  26718  resqrtcn  26719  sqrtcn  26720  loglesqrt  26731  atansopn  26902  dvatan  26905  xrlimcnp  26938  efrlim  26939  efrlimOLD  26940  lgamucov  27008  ftalem3  27045  vmcn  30778  dipcn  30799  ipasslem7  30915  ipasslem8  30916  occllem  31382  nlelchi  32140  tpr2rico  34071  rmulccn  34087  raddcn  34088  cxpcncf1  34754  cvxpconn  35438  cvxsconn  35439  cnllysconn  35441  sinccvglem  35868  ivthALT  36531  knoppcnlem10  36704  knoppcnlem11  36705  broucube  37857  dvtan  37873  ftc1cnnc  37895  dvasin  37907  dvacos  37908  dvreasin  37909  dvreacos  37910  areacirclem1  37911  areacirclem2  37912  areacirclem4  37914  refsumcn  45342  fprodcnlem  45912  fprodcn  45913  fsumcncf  46189  ioccncflimc  46196  cncfuni  46197  icocncflimc  46200  cncfdmsn  46201  cncfiooicclem1  46204  cxpcncf2  46210  fprodsub2cncf  46216  fprodadd2cncf  46217  dvmptconst  46226  dvmptidg  46228  dvresntr  46229  itgsubsticclem  46286  dirkercncflem2  46415  dirkercncflem4  46417  dirkercncf  46418  fourierdlem32  46450  fourierdlem33  46451  fourierdlem62  46479  fourierdlem93  46510  fourierdlem101  46518