Theorem cnfldtopon 24743

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ‘cfv 6502  ℂcc 11038  TopOpenctopn 17355  ℂ_fldccnfld 21326  TopOnctopon 22871  TopSpctps 22893

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 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118

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 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-1st 7945  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-er 8647  df-map 8779  df-en 8898  df-dom 8899  df-sdom 8900  df-fin 8901  df-sup 9359  df-inf 9360  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809  df-nn 12160  df-2 12222  df-3 12223  df-4 12224  df-5 12225  df-6 12226  df-7 12227  df-8 12228  df-9 12229  df-n0 12416  df-z 12503  df-dec 12622  df-uz 12766  df-q 12876  df-rp 12920  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-fz 13438  df-seq 13939  df-exp 13999  df-cj 15036  df-re 15037  df-im 15038  df-sqrt 15172  df-abs 15173  df-struct 17088  df-slot 17123  df-ndx 17135  df-base 17151  df-plusg 17204  df-mulr 17205  df-starv 17206  df-tset 17210  df-ple 17211  df-ds 17213  df-unif 17214  df-rest 17356  df-topn 17357  df-topgen 17377  df-psmet 21318  df-xmet 21319  df-met 21320  df-bl 21321  df-mopn 21322  df-cnfld 21327  df-top 22855  df-topon 22872  df-topsp 22894  df-bases 22907  df-xms 24281  df-ms 24282

This theorem is referenced by:  cnfldtop  24744  unicntop  24746  sszcld  24779  reperflem  24780  cnperf  24782  divcnOLD  24830  divcn  24832  fsumcn  24834  expcn  24836  divccn  24837  expcnOLD  24838  divccnOLD  24839  cncfcn1  24877  cncfmptc  24878  cncfmptid  24879  cncfmpt2f  24881  cdivcncf  24887  abscncfALT  24891  cncfcnvcn  24892  cnmptre  24894  iirevcn  24897  iihalf1cn  24899  iihalf1cnOLD  24900  iihalf2cn  24902  iihalf2cnOLD  24903  iimulcn  24907  iimulcnOLD  24908  icchmeo  24911  icchmeoOLD  24912  cnrehmeo  24924  cnrehmeoOLD  24925  cnheiborlem  24926  cnheibor  24927  cnllycmp  24928  evth  24931  evth2  24932  lebnumlem2  24934  reparphti  24969  reparphtiOLD  24970  pcoass  24997  mulcncf  25419  mbfimaopnlem  25629  limcvallem  25845  ellimc2  25851  limcnlp  25852  limcflflem  25854  limcflf  25855  limcmo  25856  limcres  25860  cnplimc  25861  cnlimc  25862  limccnp  25865  limccnp2  25866  dvbss  25875  perfdvf  25877  recnperf  25879  dvreslem  25883  dvres2lem  25884  dvres3a  25888  dvidlem  25889  dvcnp2  25894  dvcnp2OLD  25895  dvcn  25896  dvnres  25906  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvcmulf  25921  dvcobr  25922  dvcobrOLD  25923  dvcjbr  25926  dvrec  25932  dvmptid  25934  dvmptc  25935  dvmptres2  25939  dvmptcmul  25941  dvmptntr  25948  dvmptfsum  25952  dvcnvlem  25953  dvcnv  25954  dvexp3  25955  dveflem  25956  dvlipcn  25972  lhop1lem  25991  lhop2  25993  lhop  25994  dvcnvrelem2  25996  dvcnvre  25997  ftc1lem3  26018  ftc1cn  26023  plycn  26239  plycnOLD  26240  dvply1  26264  dvtaylp  26351  taylthlem1  26354  taylthlem2  26355  taylthlem2OLD  26356  ulmdvlem3  26384  psercn2  26405  psercn2OLD  26406  psercn  26409  pserdvlem2  26411  pserdv  26412  abelth  26424  pige3ALT  26502  logcn  26629  dvloglem  26630  dvlog  26633  dvlog2  26635  efopnlem2  26639  efopn  26640  logtayl  26642  dvcxp1  26722  cxpcn  26727  cxpcnOLD  26728  cxpcn2  26729  cxpcn3  26731  resqrtcn  26732  sqrtcn  26733  loglesqrt  26744  atansopn  26915  dvatan  26918  xrlimcnp  26951  efrlim  26952  efrlimOLD  26953  lgamucov  27021  ftalem3  27058  vmcn  30793  dipcn  30814  ipasslem7  30930  ipasslem8  30931  occllem  31397  nlelchi  32155  tpr2rico  34096  rmulccn  34112  raddcn  34113  cxpcncf1  34779  cvxpconn  35464  cvxsconn  35465  cnllysconn  35467  sinccvglem  35894  ivthALT  36557  knoppcnlem10  36730  knoppcnlem11  36731  broucube  37934  dvtan  37950  ftc1cnnc  37972  dvasin  37984  dvacos  37985  dvreasin  37986  dvreacos  37987  areacirclem1  37988  areacirclem2  37989  areacirclem4  37991  refsumcn  45419  fprodcnlem  45988  fprodcn  45989  fsumcncf  46265  ioccncflimc  46272  cncfuni  46273  icocncflimc  46276  cncfdmsn  46277  cncfiooicclem1  46280  cxpcncf2  46286  fprodsub2cncf  46292  fprodadd2cncf  46293  dvmptconst  46302  dvmptidg  46304  dvresntr  46305  itgsubsticclem  46362  dirkercncflem2  46491  dirkercncflem4  46493  dirkercncf  46494  fourierdlem32  46526  fourierdlem33  46527  fourierdlem62  46555  fourierdlem93  46586  fourierdlem101  46594