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

Theorem tgioo2 21870
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 2462 . 2  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
2 cnxmet 21842 . . 3  |-  ( abs 
o.  -  )  e.  ( *Met `  CC )
3 ax-resscn 9622 . . 3  |-  RR  C_  CC
4 tgioo2.1 . . . . 5  |-  J  =  ( TopOpen ` fld )
54cnfldtopn 21851 . . . 4  |-  J  =  ( MetOpen `  ( abs  o. 
-  ) )
6 eqid 2462 . . . 4  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 5, 6metrest 21588 . . 3  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  RR  C_  CC )  -> 
( Jt  RR )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) ) )
82, 3, 7mp2an 683 . 2  |-  ( Jt  RR )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
91, 8tgioo 21863 1  |-  ( topGen ` 
ran  (,) )  =  ( Jt  RR )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455    e. wcel 1898    C_ wss 3416    X. cxp 4851   ran crn 4854    |` cres 4855    o. ccom 4857   ` cfv 5601  (class class class)co 6315   CCcc 9563   RRcr 9564    - cmin 9886   (,)cioo 11664   abscabs 13346   ↾t crest 15368   TopOpenctopn 15369   topGenctg 15385   *Metcxmt 19004   MetOpencmopn 19009  ℂfldccnfld 19019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-map 7500  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-sup 7982  df-inf 7983  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-fz 11814  df-seq 12246  df-exp 12305  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-plusg 15252  df-mulr 15253  df-starv 15254  df-tset 15258  df-ple 15259  df-ds 15261  df-unif 15262  df-rest 15370  df-topn 15371  df-topgen 15391  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-cnfld 19020  df-top 19970  df-bases 19971  df-topon 19972
This theorem is referenced by:  rerest  21871  tgioo3  21872  zcld2  21882  metdcn  21907  metdscn2  21923  metdscn2OLD  21938  abscncfALT  22001  cnrehmeo  22030  rellycmp  22034  evth  22036  evth2  22037  lebnumlem2  22039  lebnumlem2OLD  22042  resscdrg  22374  retopn  22387  cncombf  22663  cnmbf  22664  dvcjbr  22952  rolle  22991  cmvth  22992  mvth  22993  dvlip  22994  dvlipcn  22995  dvlip2  22996  c1liplem1  22997  dvgt0lem1  23003  dvle  23008  dvivthlem1  23009  dvne0  23012  lhop1lem  23014  lhop2  23016  lhop  23017  dvcnvrelem1  23018  dvcnvrelem2  23019  dvcnvre  23020  dvcvx  23021  dvfsumle  23022  dvfsumabs  23024  dvfsumlem2  23028  ftc1  23043  ftc1cn  23044  ftc2  23045  ftc2ditglem  23046  itgparts  23048  itgsubstlem  23049  taylthlem2  23378  efcvx  23453  pige3  23521  dvloglem  23642  logdmopn  23643  advlog  23648  advlogexp  23649  logccv  23657  loglesqrt  23747  lgamgulmlem2  24004  ftalem3  24048  log2sumbnd  24431  nmcnc  26381  ipasslem7  26526  rmulccn  28783  raddcn  28784  broucube  32019  dvtanlemOLD  32036  ftc1cnnc  32061  ftc2nc  32071  dvasin  32073  dvacos  32074  dvreasin  32075  dvreacos  32076  areacirclem1  32077  areacirc  32082  itgpowd  36144  lhe4.4ex1a  36722  refsumcn  37391  climreeq  37731  limcresiooub  37761  limcresioolb  37762  lptioo2cn  37764  lptioo1cn  37765  limclner  37770  cncfiooicclem1  37809  jumpncnp  37814  fperdvper  37828  dvmptresicc  37829  dvresioo  37831  dvbdfbdioolem1  37838  itgsin0pilem1  37864  itgsinexplem1  37868  itgcoscmulx  37884  itgsubsticclem  37890  itgiccshift  37895  itgperiod  37896  itgsbtaddcnst  37897  dirkeritg  38002  dirkercncflem2  38004  dirkercncflem3  38005  dirkercncflem4  38006  dirkercncf  38007  fourierdlem28  38035  fourierdlem32  38040  fourierdlem33  38041  fourierdlem39  38047  fourierdlem56  38064  fourierdlem57  38065  fourierdlem58  38066  fourierdlem59  38067  fourierdlem60  38068  fourierdlem61  38069  fourierdlem62  38070  fourierdlem68  38076  fourierdlem72  38080  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem80  38088  fourierdlem94  38102  fourierdlem103  38111  fourierdlem104  38112  fourierdlem113  38121  fouriercnp  38128  fouriersw  38133  fouriercn  38134  etransclem2  38139  etransclem23  38160  etransclem35  38172  etransclem38  38175  etransclem39  38176  etransclem44  38181  etransclem45  38182  etransclem46  38183  etransclem47  38184
  Copyright terms: Public domain W3C validator