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

Theorem retop 18366
Description: The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
Assertion
Ref Expression
retop  |-  ( topGen ` 
ran  (,) )  e.  Top

Proof of Theorem retop
StepHypRef Expression
1 retopbas 18365 . 2  |-  ran  (,)  e. 
TopBases
2 tgcl 16807 . 2  |-  ( ran 
(,)  e.  TopBases  ->  ( topGen ` 
ran  (,) )  e.  Top )
31, 2ax-mp 8 1  |-  ( topGen ` 
ran  (,) )  e.  Top
Colors of variables: wff set class
Syntax hints:    e. wcel 1710   ran crn 4769   ` cfv 5334   (,)cioo 10745   topGenctg 13435   Topctop 16731   TopBasesctb 16735
This theorem is referenced by:  retopon  18368  retpsOLD  18369  retps  18370  icccld  18372  icopnfcld  18373  iocmnfcld  18374  qdensere  18375  zcld  18415  iccntr  18423  icccmp  18427  reconnlem2  18429  retopcon  18431  rectbntr0  18434  cnmpt2pc  18524  icoopnst  18535  iocopnst  18536  cnheiborlem  18550  bndth  18554  pcoass  18620  evthicc  18917  ovolicc2  18979  subopnmbl  19057  dvlip  19438  dvlip2  19440  dvne0  19456  lhop2  19460  lhop  19461  dvcnvrelem2  19463  dvcnvre  19464  ftc1  19487  taylthlem2  19851  cxpcn3  20193  tpr2rico  23466  brsiga  23803  unibrsiga  23806  elmbfmvol2  23881  sxbrsigalem3  23886  dya2iocbrsiga  23889  dya2icobrsiga  23890  dya2iocucvr  23898  sxbrsigalem1  23899  orrvcval4  23971  orrvcoel  23972  orrvccel  23973  lgamgulmlem2  24063  retopscon  24184  iccllyscon  24185  rellyscon  24186  cvmliftlem8  24227  cvmliftlem10  24229  ftc1cnnc  25514  ivthALT  25582  stoweidlem53  27125  stoweidlem57  27129  stoweidlem59  27131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-cnex 8880  ax-resscn 8881  ax-pre-lttri 8898  ax-pre-lttrn 8899
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-po 4393  df-so 4394  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-1st 6206  df-2nd 6207  df-er 6744  df-en 6949  df-dom 6950  df-sdom 6951  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-ioo 10749  df-topgen 13437  df-top 16736  df-bases 16738
  Copyright terms: Public domain W3C validator