Theorem retop 24698

Description: The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)

Assertion

Ref	Expression
retop	⊢ (topGen‘ran (,)) ∈ Top

Proof of Theorem retop

Step	Hyp	Ref	Expression
1		retopbas 24697	. 2 ⊢ ran (,) ∈ TopBases
2		tgcl 22905	. 2 ⊢ (ran (,) ∈ TopBases → (topGen‘ran (,)) ∈ Top)
3	1, 2	ax-mp 5	1 ⊢ (topGen‘ran (,)) ∈ Top

Syntax hints:   ∈ wcel 2108  ran crn 5655  ‘cfv 6530  (,)cioo 13360  topGenctg 17449  Topctop 22829  TopBasesctb 22881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-1st 7986  df-2nd 7987  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-ioo 13364  df-topgen 17455  df-top 22830  df-bases 22882

This theorem is referenced by:  retopon  24700  retps  24701  icccld  24703  icopnfcld  24704  iocmnfcld  24705  qdensere  24706  zcld  24751  iccntr  24759  icccmp  24763  reconnlem2  24765  retopconn  24767  rectbntr0  24770  cnmpopc  24871  icoopnst  24885  iocopnst  24886  cnheiborlem  24902  bndth  24906  pcoass  24973  evthicc  25410  ovolicc2  25473  subopnmbl  25555  dvlip  25948  dvlip2  25950  dvne0  25966  lhop2  25970  lhop  25971  dvcnvrelem2  25973  dvcnvre  25974  ftc1  25999  taylthlem2  26332  taylthlem2OLD  26333  cxpcn3  26708  lgamgulmlem2  26990  circtopn  33814  tpr2rico  33889  rrhqima  33991  rrhre  33998  brsiga  34160  unibrsiga  34163  elmbfmvol2  34245  sxbrsigalem3  34250  dya2iocbrsiga  34253  dya2icobrsiga  34254  dya2iocucvr  34262  sxbrsigalem1  34263  orrvcval4  34443  orrvcoel  34444  orrvccel  34445  retopsconn  35217  iccllysconn  35218  rellysconn  35219  cvmliftlem8  35260  cvmliftlem10  35262  ivthALT  36299  ptrecube  37590  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimir  37623  broucube  37624  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  cnambfre  37638  ftc1cnnc  37662  dvrelog3  42024  redvmptabs  42350  reopn  45266  ioontr  45488  iocopn  45497  icoopn  45502  limciccioolb  45598  limcicciooub  45614  lptre2pt  45617  limcresiooub  45619  limcresioolb  45620  limclner  45628  limclr  45632  icccncfext  45864  cncfiooicclem1  45870  fperdvper  45896  stoweidlem53  46030  stoweidlem57  46034  dirkercncflem2  46081  dirkercncflem3  46082  dirkercncflem4  46083  fourierdlem32  46116  fourierdlem33  46117  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem58  46141  fourierdlem62  46145  fourierdlem73  46156  fouriersw  46208  iooborel  46328  bor1sal  46332  incsmf  46719  decsmf  46744  smfpimbor1lem2  46776  smf2id  46778  smfco  46779  iooii  48840