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

Theorem cnfldtopon 22526
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
StepHypRef Expression
1 cnfldtps 22521 . 2 fld ∈ TopSp
2 cnfldbas 19690 . . 3 ℂ = (Base‘ℂfld)
3 cnfldtopn.1 . . 3 𝐽 = (TopOpen‘ℂfld)
42, 3istps 20678 . 2 (ℂfld ∈ TopSp ↔ 𝐽 ∈ (TopOn‘ℂ))
51, 4mpbi 220 1 𝐽 ∈ (TopOn‘ℂ)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  cfv 5857  cc 9894  TopOpenctopn 16022  fldccnfld 19686  TopOnctopon 20655  TopSpctps 20676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-map 7819  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-inf 8309  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-fz 12285  df-seq 12758  df-exp 12817  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-plusg 15894  df-mulr 15895  df-starv 15896  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-rest 16023  df-topn 16024  df-topgen 16044  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-xms 22065  df-ms 22066
This theorem is referenced by:  cnfldtop  22527  unicntop  22529  sszcld  22560  reperflem  22561  cnperf  22563  divcn  22611  fsumcn  22613  expcn  22615  divccn  22616  cncfcn1  22653  cncfmptc  22654  cncfmptid  22655  cncfmpt2f  22657  cdivcncf  22660  abscncfALT  22663  cncfcnvcn  22664  cnmptre  22666  iirevcn  22669  iihalf1cn  22671  iihalf2cn  22673  iimulcn  22677  icchmeo  22680  cnrehmeo  22692  cnheiborlem  22693  cnheibor  22694  cnllycmp  22695  evth  22698  evth2  22699  lebnumlem2  22701  reparphti  22737  pcoass  22764  csscld  22988  clsocv  22989  cncmet  23059  resscdrg  23094  mbfimaopnlem  23362  limcvallem  23575  ellimc2  23581  limcnlp  23582  limcflflem  23584  limcflf  23585  limcmo  23586  limcres  23590  cnplimc  23591  cnlimc  23592  limccnp  23595  limccnp2  23596  limciun  23598  dvbss  23605  perfdvf  23607  recnperf  23609  dvreslem  23613  dvres2lem  23614  dvres3a  23618  dvidlem  23619  dvcnp2  23623  dvcn  23624  dvnres  23634  dvaddbr  23641  dvmulbr  23642  dvcmulf  23648  dvcobr  23649  dvcjbr  23652  dvrec  23658  dvmptid  23660  dvmptc  23661  dvmptres2  23665  dvmptcmul  23667  dvmptntr  23674  dvmptfsum  23676  dvcnvlem  23677  dvcnv  23678  dvexp3  23679  dveflem  23680  dvlipcn  23695  lhop1lem  23714  lhop2  23716  lhop  23717  dvcnvrelem2  23719  dvcnvre  23720  ftc1lem3  23739  ftc1cn  23744  plycn  23955  dvply1  23977  dvtaylp  24062  taylthlem1  24065  taylthlem2  24066  ulmdvlem3  24094  psercn2  24115  psercn  24118  pserdvlem2  24120  pserdv  24121  abelth  24133  pige3  24207  logcn  24327  dvloglem  24328  logdmopn  24329  dvlog  24331  dvlog2  24333  efopnlem2  24337  efopn  24338  logtayl  24340  dvcxp1  24415  cxpcn  24420  cxpcn2  24421  cxpcn3  24423  resqrtcn  24424  sqrtcn  24425  loglesqrt  24433  atansopn  24593  dvatan  24596  xrlimcnp  24629  efrlim  24630  lgamucov  24698  lgamucov2  24699  ftalem3  24735  vmcn  27442  dipcn  27463  ipasslem7  27579  ipasslem8  27580  occllem  28050  nlelchi  28808  tpr2rico  29782  rmulccn  29798  raddcn  29799  cvxpconn  30985  cvxsconn  30986  cnllysconn  30988  sinccvglem  31327  ivthALT  32025  knoppcnlem10  32187  knoppcnlem11  32188  broucube  33114  dvtanlem  33130  dvtan  33131  ftc1cnnc  33155  dvasin  33167  dvacos  33168  dvreasin  33169  dvreacos  33170  areacirclem1  33171  areacirclem2  33172  areacirclem4  33174  refsumcn  38711  fprodcnlem  39267  fprodcn  39268  fsumcncf  39426  ioccncflimc  39433  cncfuni  39434  icocncflimc  39437  cncfdmsn  39438  cncfiooicclem1  39441  cxpcncf2  39448  fprodsub2cncf  39454  fprodadd2cncf  39455  dvmptconst  39465  dvmptidg  39467  dvresntr  39468  itgsubsticclem  39528  dirkercncflem2  39658  dirkercncflem4  39660  dirkercncf  39661  fourierdlem32  39693  fourierdlem33  39694  fourierdlem62  39722  fourierdlem93  39753  fourierdlem101  39761
  Copyright terms: Public domain W3C validator