MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfldtop Structured version   Visualization version   Unicode version

Theorem cnfldtop 21814
Description: The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypothesis
Ref Expression
cnfldtopn.1  |-  J  =  ( TopOpen ` fld )
Assertion
Ref Expression
cnfldtop  |-  J  e. 
Top

Proof of Theorem cnfldtop
StepHypRef Expression
1 cnfldtopn.1 . . 3  |-  J  =  ( TopOpen ` fld )
21cnfldtopon 21813 . 2  |-  J  e.  (TopOn `  CC )
32topontopi 19956 1  |-  J  e. 
Top
Colors of variables: wff setvar class
Syntax hints:    = wceq 1447    e. wcel 1890   ` cfv 5560   CCcc 9523   TopOpenctopn 15330  ℂfldccnfld 18980   Topctop 19927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602  ax-pre-sup 9603
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-1st 6780  df-2nd 6781  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-1o 7168  df-oadd 7172  df-er 7349  df-map 7460  df-en 7556  df-dom 7557  df-sdom 7558  df-fin 7559  df-sup 7942  df-inf 7943  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-div 10258  df-nn 10598  df-2 10656  df-3 10657  df-4 10658  df-5 10659  df-6 10660  df-7 10661  df-8 10662  df-9 10663  df-10 10664  df-n0 10859  df-z 10927  df-dec 11041  df-uz 11149  df-q 11254  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-fz 11775  df-seq 12207  df-exp 12266  df-cj 13172  df-re 13173  df-im 13174  df-sqrt 13308  df-abs 13309  df-struct 15133  df-ndx 15134  df-slot 15135  df-base 15136  df-plusg 15213  df-mulr 15214  df-starv 15215  df-tset 15219  df-ple 15220  df-ds 15222  df-unif 15223  df-rest 15331  df-topn 15332  df-topgen 15352  df-psmet 18972  df-xmet 18973  df-met 18974  df-bl 18975  df-mopn 18976  df-cnfld 18981  df-top 19931  df-bases 19932  df-topon 19933  df-topsp 19934  df-xms 21345  df-ms 21346
This theorem is referenced by:  rerest  21832  recld2  21842  zdis  21844  reperflem  21846  metdcn  21868  metdscn2  21884  metdscn2OLD  21899  cncfcn1  21952  cncfcnvcn  21963  icchmeo  21979  cnrehmeo  21991  cnheiborlem  21992  cnheibor  21993  cnllycmp  21994  evth  21997  reparphti  22038  cncmet  22300  resscdrg  22335  mbfimaopn2  22624  ellimc2  22843  limcnlp  22844  limcflflem  22846  limcflf  22847  limccnp  22857  limciun  22860  dvbss  22867  perfdvf  22869  dvreslem  22875  dvres2lem  22876  dvidlem  22881  dvcnp2  22885  dvnres  22896  dvaddbr  22903  dvmulbr  22904  dvrec  22920  dvmptres  22928  dvexp3  22941  dveflem  22942  dvlipcn  22957  dvcnvrelem2  22981  ftc1cn  23006  dvply1  23248  ulmdvlem3  23368  psercn  23392  pserdvlem2  23394  pserdv  23395  abelth  23407  logcn  23603  dvloglem  23604  dvlog  23607  dvlog2  23609  efopnlem2  23613  efopn  23614  logtayl  23616  dvatan  23872  efrlim  23906  lgamucov  23974  lgamucov2  23975  ftalem3  24010  nmcnc  26343  raddcn  28741  lmlim  28759  cvxpcon  29970  cvxscon  29971  cnllyscon  29973  ivthALT  30996  broucube  31975  ftc1cnnc  32017  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  cnopn  37369  climreeq  37734  limcrecl  37750  islpcn  37760  limcresiooub  37764  limcresioolb  37765  lptioo2cn  37767  lptioo1cn  37768  limclner  37773  fsumcncf  37796  ioccncflimc  37804  cncfuni  37805  icocncflimc  37808  cncfiooicclem1  37812  cncfiooicc  37813  itgsubsticclem  37893  dirkercncflem2  38022  dirkercncflem4  38024  dirkercncf  38025  fourierdlem32  38058  fourierdlem33  38059  fourierdlem48  38074  fourierdlem49  38075  fourierdlem62  38088  fourierdlem93  38119  fourierdlem101  38127  fourierdlem113  38139  fouriercnp  38146  fouriersw  38151
  Copyright terms: Public domain W3C validator