Theorem cnfldtop 24764

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 24763	. 2 ⊢ 𝐽 ∈ (TopOn‘ℂ)
3	2	topontopi 22896	1 ⊢ 𝐽 ∈ Top

Syntax hints:   = wceq 1542   ∈ wcel 2114  ‘cfv 6496  ℂcc 11033  TopOpenctopn 17381  ℂ_fldccnfld 21350  Topctop 22874

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 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112  ax-pre-sup 11113

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-om 7815  df-1st 7939  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-er 8640  df-map 8772  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9352  df-inf 9353  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-div 11805  df-nn 12172  df-2 12241  df-3 12242  df-4 12243  df-5 12244  df-6 12245  df-7 12246  df-8 12247  df-9 12248  df-n0 12435  df-z 12522  df-dec 12642  df-uz 12786  df-q 12896  df-rp 12940  df-xneg 13060  df-xadd 13061  df-xmul 13062  df-fz 13459  df-seq 13961  df-exp 14021  df-cj 15058  df-re 15059  df-im 15060  df-sqrt 15194  df-abs 15195  df-struct 17114  df-slot 17149  df-ndx 17161  df-base 17177  df-plusg 17230  df-mulr 17231  df-starv 17232  df-tset 17236  df-ple 17237  df-ds 17239  df-unif 17240  df-rest 17382  df-topn 17383  df-topgen 17403  df-psmet 21342  df-xmet 21343  df-met 21344  df-bl 21345  df-mopn 21346  df-cnfld 21351  df-top 22875  df-topon 22892  df-topsp 22914  df-bases 22927  df-xms 24301  df-ms 24302

This theorem is referenced by:  cnopn  24767  rerest  24785  recld2  24796  zdis  24798  reperflem  24800  metdcn  24822  ngnmcncn  24827  metdscn2  24839  cncfcnvcn  24908  icchmeo  24924  cnrehmeo  24936  cnheiborlem  24937  cnheibor  24938  cnllycmp  24939  evth  24942  reparphti  24980  cncmet  25305  resscdrg  25341  mbfimaopn2  25640  ellimc2  25860  limcnlp  25861  limcflflem  25863  limcflf  25864  limccnp  25874  limciun  25877  dvbss  25884  perfdvf  25886  dvreslem  25892  dvres2lem  25893  dvidlem  25898  dvcnp2  25903  dvnres  25914  dvaddbr  25921  dvmulbr  25922  dvrec  25938  dvmptres  25946  dveflem  25962  dvlipcn  25977  dvcnvrelem2  26001  dvply1  26266  ulmdvlem3  26386  psercn  26410  abelth  26425  dvlog  26634  dvlog2  26636  efopnlem2  26640  efopn  26641  efrlim  26952  efrlimOLD  26953  lgamucov  27021  lgamucov2  27022  nmcnc  30788  raddcn  34095  lmlim  34113  cvxpconn  35446  cvxsconn  35447  cnllysconn  35449  ivthALT  36539  knoppcnlem10  36784  broucube  37997  binomcxplemdvbinom  44806  binomcxplemnotnn0  44809  climreeq  46069  limcrecl  46085  islpcn  46093  limcresiooub  46096  limcresioolb  46097  lptioo2cn  46099  lptioo1cn  46100  limclner  46105  fsumcncf  46332  ioccncflimc  46339  cncfuni  46340  icocncflimc  46343  cncfiooicclem1  46347  cncfiooicc  46348  itgsubsticclem  46429  dirkercncflem2  46558  dirkercncflem4  46560  dirkercncf  46561  fourierdlem32  46593  fourierdlem33  46594  fourierdlem48  46608  fourierdlem49  46609  fourierdlem62  46622  fourierdlem93  46653  fourierdlem101  46661  fourierdlem113  46673  fouriercnp  46680  fouriersw  46685