Theorem cnfldtopon 25102

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  ℂcc 11199  TopOpenctopn 17593  ℂ_fldccnfld 21679  TopOnctopon 23229  TopSpctps 23251

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11257  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277  ax-pre-mulgt0 11278  ax-pre-sup 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8300  df-wrecs 8331  df-recs 8380  df-rdg 8419  df-1o 8477  df-er 8718  df-map 8850  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-sup 9435  df-inf 9436  df-pnf 11346  df-mnf 11347  df-xr 11348  df-ltxr 11349  df-le 11350  df-sub 11544  df-neg 11545  df-div 11975  df-nn 12337  df-2 12406  df-3 12407  df-4 12408  df-5 12409  df-6 12410  df-7 12411  df-8 12412  df-9 12413  df-n0 12608  df-z 12695  df-dec 12816  df-uz 12967  df-q 13077  df-rp 13122  df-xneg 13242  df-xadd 13243  df-xmul 13244  df-fz 13641  df-seq 14146  df-exp 14206  df-cj 15267  df-re 15268  df-im 15269  df-sqrt 15403  df-abs 15404  df-struct 17326  df-slot 17361  df-ndx 17373  df-base 17389  df-plusg 17442  df-mulr 17443  df-starv 17444  df-tset 17448  df-ple 17449  df-ds 17451  df-unif 17452  df-rest 17594  df-topn 17595  df-topgen 17615  df-psmet 21671  df-xmet 21672  df-met 21673  df-bl 21674  df-mopn 21675  df-cnfld 21680  df-top 23213  df-topon 23230  df-topsp 23252  df-bases 23265  df-xms 24640  df-ms 24641

This theorem is used by:  cnfldtop  25103  unicntop  25105  sszcld  25138  reperflem  25139  cnperf  25141  divcn  25190  fsumcn  25192  expcn  25194  divccn  25195  cncfcn1  25233  cncfmptc  25234  cncfmptid  25235  cncfmpt2f  25237  cdivcncf  25243  abscncfALT  25246  cncfcnvcn  25247  cnmptre  25249  iirevcn  25252  iihalf1cn  25254  iihalf2cn  25256  iimulcn  25260  icchmeo  25263  cnrehmeo  25275  cnheiborlem  25276  cnheibor  25277  cnllycmp  25278  evth  25281  evth2  25282  lebnumlem2  25284  reparphti  25319  pcoass  25346  mulcncf  25768  mbfimaopnlem  25977  limcvallem  26192  ellimc2  26198  limcnlp  26199  limcflflem  26201  limcflf  26202  limcmo  26203  limcres  26207  cnplimc  26208  cnlimc  26209  limccnp  26212  limccnp2  26213  dvbss  26222  perfdvf  26224  recnperf  26226  dvreslem  26230  dvres2lem  26231  dvres3a  26235  dvidlem  26236  dvcnp2  26241  dvcn  26242  dvnres  26252  dvaddbr  26259  dvmulbr  26260  dvcmulf  26266  dvcobr  26267  dvcjbr  26270  dvrec  26276  dvmptid  26278  dvmptc  26279  dvmptres2  26283  dvmptcmul  26285  dvmptntr  26292  dvmptfsum  26296  dvcnvlem  26297  dvcnv  26298  dvexp3  26299  dveflem  26300  dvlipcn  26315  lhop1lem  26334  lhop2  26336  lhop  26337  dvcnvrelem2  26339  dvcnvre  26340  ftc1lem3  26359  ftc1cn  26364  plycn  26581  dvply1  26606  dvtaylp  26698  taylthlem1  26701  taylthlem2  26702  ulmdvlem3  26730  psercn2  26751  psercn  26754  pserdvlem2  26756  pserdv  26757  abelth  26769  pige3ALT  26849  logcn  26976  dvloglem  26977  dvlog  26980  dvlog2  26982  efopnlem2  26986  efopn  26987  logtayl  26989  dvcxp1  27069  cxpcn  27074  cxpcn2  27075  cxpcn3  27077  resqrtcn  27078  sqrtcn  27079  loglesqrt  27090  atansopn  27261  dvatan  27264  xrlimcnp  27297  efrlim  27298  lgamucov  27366  ftalem3  27403  vmcn  31302  dipcn  31323  ipasslem7  31439  ipasslem8  31440  occllem  31906  nlelchi  32664  tpr2rico  34587  rmulccn  34603  raddcn  34604  cxpcncf1  35267  cvxpconn  36050  cvxsconn  36051  cnllysconn  36053  sinccvglem  36480  ivthALT  37166  knoppcnlem10  37411  knoppcnlem11  37412  broucube  38616  dvtan  38632  ftc1cnnc  38654  dvasin  38666  dvacos  38667  dvreasin  38668  dvreacos  38669  areacirclem1  38670  areacirclem2  38671  areacirclem4  38673  refsumcn  46091  fprodcnlem  46655  fprodcn  46656  fsumcncf  46932  ioccncflimc  46939  cncfuni  46940  icocncflimc  46943  cncfdmsn  46944  cncfiooicclem1  46947  cxpcncf2  46953  fprodsub2cncf  46959  fprodadd2cncf  46960  dvmptconst  46969  dvmptidg  46971  dvresntr  46972  itgsubsticclem  47029  dirkercncflem2  47158  dirkercncflem4  47160  dirkercncf  47161  fourierdlem32  47193  fourierdlem33  47194  fourierdlem62  47222  fourierdlem93  47253  fourierdlem101  47261  dvsec  50900  dvcsc  50901  dvcot  50902