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

Theorem retop 22478
Description: The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
Assertion
Ref Expression
retop (topGen‘ran (,)) ∈ Top

Proof of Theorem retop
StepHypRef Expression
1 retopbas 22477 . 2 ran (,) ∈ TopBases
2 tgcl 20687 . 2 (ran (,) ∈ TopBases → (topGen‘ran (,)) ∈ Top)
31, 2ax-mp 5 1 (topGen‘ran (,)) ∈ Top
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  ran crn 5077  cfv 5849  (,)cioo 12120  topGenctg 16022  Topctop 20620  TopBasesctb 20663
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-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-pre-lttri 9957  ax-pre-lttrn 9958
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 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-po 4997  df-so 4998  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-1st 7116  df-2nd 7117  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-ioo 12124  df-topgen 16028  df-top 20621  df-bases 20664
This theorem is referenced by:  retopon  22480  retps  22481  icccld  22483  icopnfcld  22484  iocmnfcld  22485  qdensere  22486  zcld  22529  iccntr  22537  icccmp  22541  reconnlem2  22543  retopconn  22545  rectbntr0  22548  cnmpt2pc  22640  icoopnst  22651  iocopnst  22652  cnheiborlem  22666  bndth  22670  pcoass  22737  evthicc  23141  ovolicc2  23203  subopnmbl  23285  dvlip  23667  dvlip2  23669  dvne0  23685  lhop2  23689  lhop  23690  dvcnvrelem2  23692  dvcnvre  23693  ftc1  23716  taylthlem2  24039  cxpcn3  24396  lgamgulmlem2  24663  circtopn  29698  tpr2rico  29752  rrhqima  29852  rrhre  29859  brsiga  30039  unibrsiga  30042  elmbfmvol2  30122  sxbrsigalem3  30127  dya2iocbrsiga  30130  dya2icobrsiga  30131  dya2iocucvr  30139  sxbrsigalem1  30140  orrvcval4  30319  orrvcoel  30320  orrvccel  30321  retopsconn  30960  iccllysconn  30961  rellysconn  30962  cvmliftlem8  31003  cvmliftlem10  31005  ivthALT  31993  ptrecube  33062  poimirlem29  33091  poimirlem30  33092  poimirlem31  33093  poimir  33095  broucube  33096  mblfinlem1  33099  mblfinlem2  33100  mblfinlem3  33101  mblfinlem4  33102  ismblfin  33103  cnambfre  33111  ftc1cnnc  33137  reopn  38983  ioontr  39165  iocopn  39175  icoopn  39180  limciccioolb  39275  limcicciooub  39291  lptre2pt  39294  limcresiooub  39296  limcresioolb  39297  limclner  39305  limclr  39309  icccncfext  39421  cncfiooicclem1  39427  fperdvper  39456  stoweidlem53  39593  stoweidlem57  39597  stoweidlem59  39599  dirkercncflem2  39644  dirkercncflem3  39645  dirkercncflem4  39646  fourierdlem32  39679  fourierdlem33  39680  fourierdlem42  39689  fourierdlem48  39694  fourierdlem49  39695  fourierdlem58  39704  fourierdlem62  39708  fourierdlem73  39719  fouriersw  39771  iooborel  39892  bor1sal  39896  incsmf  40274  decsmf  40298  smfpimbor1lem2  40329  smf2id  40331  smfco  40332
  Copyright terms: Public domain W3C validator