Theorem cnfldtop 24731

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
cnfldtop	⊢ 𝐽 ∈ Top

Proof of Theorem cnfldtop

Step	Hyp	Ref	Expression
1		cnfldtopn.1	. . 3 ⊢ 𝐽 = (TopOpen‘ℂfld)
2	1	cnfldtopon 24730	. 2 ⊢ 𝐽 ∈ (TopOn‘ℂ)
3	2	topontopi 22863	1 ⊢ 𝐽 ∈ Top

Syntax hints:   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  ℂcc 11028  TopOpenctopn 17345  ℂ_fldccnfld 21313  Topctop 22841

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:  cnopn  24734  rerest  24752  recld2  24763  zdis  24765  reperflem  24767  metdcn  24789  ngnmcncn  24794  metdscn2  24806  cncfcnvcn  24879  icchmeo  24898  icchmeoOLD  24899  cnrehmeo  24911  cnrehmeoOLD  24912  cnheiborlem  24913  cnheibor  24914  cnllycmp  24915  evth  24918  reparphti  24956  reparphtiOLD  24957  cncmet  25282  resscdrg  25318  mbfimaopn2  25618  ellimc2  25838  limcnlp  25839  limcflflem  25841  limcflf  25842  limccnp  25852  limciun  25855  dvbss  25862  perfdvf  25864  dvreslem  25870  dvres2lem  25871  dvidlem  25876  dvcnp2  25881  dvcnp2OLD  25882  dvnres  25893  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvrec  25919  dvmptres  25927  dveflem  25943  dvlipcn  25959  dvcnvrelem2  25983  dvply1  26251  ulmdvlem3  26371  psercn  26396  abelth  26411  dvlog  26620  dvlog2  26622  efopnlem2  26626  efopn  26627  efrlim  26939  efrlimOLD  26940  lgamucov  27008  lgamucov2  27009  nmcnc  30775  raddcn  34088  lmlim  34106  cvxpconn  35438  cvxsconn  35439  cnllysconn  35441  ivthALT  36531  knoppcnlem10  36704  broucube  37857  binomcxplemdvbinom  44661  binomcxplemnotnn0  44664  climreeq  45926  limcrecl  45942  islpcn  45950  limcresiooub  45953  limcresioolb  45954  lptioo2cn  45956  lptioo1cn  45957  limclner  45962  fsumcncf  46189  ioccncflimc  46196  cncfuni  46197  icocncflimc  46200  cncfiooicclem1  46204  cncfiooicc  46205  itgsubsticclem  46286  dirkercncflem2  46415  dirkercncflem4  46417  dirkercncf  46418  fourierdlem32  46450  fourierdlem33  46451  fourierdlem48  46465  fourierdlem49  46466  fourierdlem62  46479  fourierdlem93  46510  fourierdlem101  46518  fourierdlem113  46530  fouriercnp  46537  fouriersw  46542