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

Theorem retop 22687
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 22686 . 2 ran (,) ∈ TopBases
2 tgcl 20896 . 2 (ran (,) ∈ TopBases → (topGen‘ran (,)) ∈ Top)
31, 2ax-mp 5 1 (topGen‘ran (,)) ∈ Top
Colors of variables: wff setvar class
Syntax hints:  wcel 2103  ran crn 5219  cfv 6001  (,)cioo 12289  topGenctg 16221  Topctop 20821  TopBasesctb 20872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-pre-lttri 10123  ax-pre-lttrn 10124
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-po 5139  df-so 5140  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-1st 7285  df-2nd 7286  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-ioo 12293  df-topgen 16227  df-top 20822  df-bases 20873
This theorem is referenced by:  retopon  22689  retps  22690  icccld  22692  icopnfcld  22693  iocmnfcld  22694  qdensere  22695  zcld  22738  iccntr  22746  icccmp  22750  reconnlem2  22752  retopconn  22754  rectbntr0  22757  cnmpt2pc  22849  icoopnst  22860  iocopnst  22861  cnheiborlem  22875  bndth  22879  pcoass  22945  evthicc  23349  ovolicc2  23411  subopnmbl  23493  dvlip  23876  dvlip2  23878  dvne0  23894  lhop2  23898  lhop  23899  dvcnvrelem2  23901  dvcnvre  23902  ftc1  23925  taylthlem2  24248  cxpcn3  24609  lgamgulmlem2  24876  circtopn  30134  tpr2rico  30188  rrhqima  30288  rrhre  30295  brsiga  30476  unibrsiga  30479  elmbfmvol2  30559  sxbrsigalem3  30564  dya2iocbrsiga  30567  dya2icobrsiga  30568  dya2iocucvr  30576  sxbrsigalem1  30577  orrvcval4  30756  orrvcoel  30757  orrvccel  30758  retopsconn  31459  iccllysconn  31460  rellysconn  31461  cvmliftlem8  31502  cvmliftlem10  31504  ivthALT  32557  ptrecube  33641  poimirlem29  33670  poimirlem30  33671  poimirlem31  33672  poimir  33674  broucube  33675  mblfinlem1  33678  mblfinlem2  33679  mblfinlem3  33680  mblfinlem4  33681  ismblfin  33682  cnambfre  33690  ftc1cnnc  33716  reopn  39917  ioontr  40156  iocopn  40166  icoopn  40171  limciccioolb  40273  limcicciooub  40289  lptre2pt  40292  limcresiooub  40294  limcresioolb  40295  limclner  40303  limclr  40307  icccncfext  40520  cncfiooicclem1  40526  fperdvper  40553  stoweidlem53  40690  stoweidlem57  40694  dirkercncflem2  40741  dirkercncflem3  40742  dirkercncflem4  40743  fourierdlem32  40776  fourierdlem33  40777  fourierdlem42  40786  fourierdlem48  40791  fourierdlem49  40792  fourierdlem58  40801  fourierdlem62  40805  fourierdlem73  40816  fouriersw  40868  iooborel  40989  bor1sal  40993  incsmf  41374  decsmf  41398  smfpimbor1lem2  41429  smf2id  41431  smfco  41432
  Copyright terms: Public domain W3C validator