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

Theorem tgioo2 21758
Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.)
Hypothesis
Ref Expression
tgioo2.1  |-  J  =  ( TopOpen ` fld )
Assertion
Ref Expression
tgioo2  |-  ( topGen ` 
ran  (,) )  =  ( Jt  RR )

Proof of Theorem tgioo2
StepHypRef Expression
1 eqid 2423 . 2  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
2 cnxmet 21730 . . 3  |-  ( abs 
o.  -  )  e.  ( *Met `  CC )
3 ax-resscn 9542 . . 3  |-  RR  C_  CC
4 tgioo2.1 . . . . 5  |-  J  =  ( TopOpen ` fld )
54cnfldtopn 21739 . . . 4  |-  J  =  ( MetOpen `  ( abs  o. 
-  ) )
6 eqid 2423 . . . 4  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 5, 6metrest 21476 . . 3  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  RR  C_  CC )  -> 
( Jt  RR )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) ) )
82, 3, 7mp2an 676 . 2  |-  ( Jt  RR )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
91, 8tgioo 21751 1  |-  ( topGen ` 
ran  (,) )  =  ( Jt  RR )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872    C_ wss 3374    X. cxp 4789   ran crn 4792    |` cres 4793    o. ccom 4795   ` cfv 5539  (class class class)co 6244   CCcc 9483   RRcr 9484    - cmin 9806   (,)cioo 11581   abscabs 13236   ↾t crest 15257   TopOpenctopn 15258   topGenctg 15274   *Metcxmt 18893   MetOpencmopn 18898  ℂfldccnfld 18908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-sup 7904  df-inf 7905  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-4 10616  df-5 10617  df-6 10618  df-7 10619  df-8 10620  df-9 10621  df-10 10622  df-n0 10816  df-z 10884  df-dec 10998  df-uz 11106  df-q 11211  df-rp 11249  df-xneg 11355  df-xadd 11356  df-xmul 11357  df-ioo 11585  df-fz 11731  df-seq 12159  df-exp 12218  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-plusg 15141  df-mulr 15142  df-starv 15143  df-tset 15147  df-ple 15148  df-ds 15150  df-unif 15151  df-rest 15259  df-topn 15260  df-topgen 15280  df-psmet 18900  df-xmet 18901  df-met 18902  df-bl 18903  df-mopn 18904  df-cnfld 18909  df-top 19858  df-bases 19859  df-topon 19860
This theorem is referenced by:  rerest  21759  tgioo3  21760  zcld2  21770  metdcn  21795  metdscn2  21811  metdscn2OLD  21826  abscncfALT  21889  cnrehmeo  21918  rellycmp  21922  evth  21924  evth2  21925  lebnumlem2  21927  lebnumlem2OLD  21930  resscdrg  22262  retopn  22275  cncombf  22551  cnmbf  22552  dvcjbr  22840  rolle  22879  cmvth  22880  mvth  22881  dvlip  22882  dvlipcn  22883  dvlip2  22884  c1liplem1  22885  dvgt0lem1  22891  dvle  22896  dvivthlem1  22897  dvne0  22900  lhop1lem  22902  lhop2  22904  lhop  22905  dvcnvrelem1  22906  dvcnvrelem2  22907  dvcnvre  22908  dvcvx  22909  dvfsumle  22910  dvfsumabs  22912  dvfsumlem2  22916  ftc1  22931  ftc1cn  22932  ftc2  22933  ftc2ditglem  22934  itgparts  22936  itgsubstlem  22937  taylthlem2  23266  efcvx  23341  pige3  23409  dvloglem  23530  logdmopn  23531  advlog  23536  advlogexp  23537  logccv  23545  loglesqrt  23635  lgamgulmlem2  23892  ftalem3  23936  log2sumbnd  24319  nmcnc  26269  ipasslem7  26414  rmulccn  28681  raddcn  28682  broucube  31881  dvtanlemOLD  31898  ftc1cnnc  31923  ftc2nc  31933  dvasin  31935  dvacos  31936  dvreasin  31937  dvreacos  31938  areacirclem1  31939  areacirc  31944  itgpowd  36012  lhe4.4ex1a  36591  refsumcn  37267  climreeq  37576  limcresiooub  37606  limcresioolb  37607  lptioo2cn  37609  lptioo1cn  37610  limclner  37615  cncfiooicclem1  37654  jumpncnp  37659  fperdvper  37673  dvmptresicc  37674  dvresioo  37676  dvbdfbdioolem1  37683  itgsin0pilem1  37709  itgsinexplem1  37713  itgcoscmulx  37729  itgsubsticclem  37735  itgiccshift  37740  itgperiod  37741  itgsbtaddcnst  37742  dirkeritg  37847  dirkercncflem2  37849  dirkercncflem3  37850  dirkercncflem4  37851  dirkercncf  37852  fourierdlem28  37880  fourierdlem32  37885  fourierdlem33  37886  fourierdlem39  37892  fourierdlem56  37909  fourierdlem57  37910  fourierdlem58  37911  fourierdlem59  37912  fourierdlem60  37913  fourierdlem61  37914  fourierdlem62  37915  fourierdlem68  37921  fourierdlem72  37925  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem80  37933  fourierdlem94  37947  fourierdlem103  37956  fourierdlem104  37957  fourierdlem113  37966  fouriercnp  37973  fouriersw  37978  fouriercn  37979  etransclem2  37984  etransclem23  38005  etransclem35  38017  etransclem38  38020  etransclem39  38021  etransclem44  38026  etransclem45  38027  etransclem46  38028  etransclem47  38029
  Copyright terms: Public domain W3C validator