Theorem retop 24671

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 24670	. 2 ⊢ ran (,) ∈ TopBases
2		tgcl 22879	. 2 ⊢ (ran (,) ∈ TopBases → (topGen‘ran (,)) ∈ Top)
3	1, 2	ax-mp 5	1 ⊢ (topGen‘ran (,)) ∈ Top

Syntax hints:   ∈ wcel 2111  ran crn 5612  ‘cfv 6476  (,)cioo 13240  topGenctg 17336  Topctop 22803  TopBasesctb 22855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058  ax-pre-lttri 11075  ax-pre-lttrn 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-po 5519  df-so 5520  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-oprab 7345  df-mpo 7346  df-1st 7916  df-2nd 7917  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-ioo 13244  df-topgen 17342  df-top 22804  df-bases 22856

This theorem is referenced by:  retopon  24673  retps  24674  icccld  24676  icopnfcld  24677  iocmnfcld  24678  qdensere  24679  zcld  24724  iccntr  24732  icccmp  24736  reconnlem2  24738  retopconn  24740  rectbntr0  24743  cnmpopc  24844  icoopnst  24858  iocopnst  24859  cnheiborlem  24875  bndth  24879  pcoass  24946  evthicc  25382  ovolicc2  25445  subopnmbl  25527  dvlip  25920  dvlip2  25922  dvne0  25938  lhop2  25942  lhop  25943  dvcnvrelem2  25945  dvcnvre  25946  ftc1  25971  taylthlem2  26304  taylthlem2OLD  26305  cxpcn3  26680  lgamgulmlem2  26962  circtopn  33842  tpr2rico  33917  rrhqima  34019  rrhre  34026  brsiga  34188  unibrsiga  34191  elmbfmvol2  34272  sxbrsigalem3  34277  dya2iocbrsiga  34280  dya2icobrsiga  34281  dya2iocucvr  34289  sxbrsigalem1  34290  orrvcval4  34470  orrvcoel  34471  orrvccel  34472  retopsconn  35285  iccllysconn  35286  rellysconn  35287  cvmliftlem8  35328  cvmliftlem10  35330  ivthALT  36369  ptrecube  37660  poimirlem29  37689  poimirlem30  37690  poimirlem31  37691  poimir  37693  broucube  37694  mblfinlem1  37697  mblfinlem2  37698  mblfinlem3  37699  mblfinlem4  37700  ismblfin  37701  cnambfre  37708  ftc1cnnc  37732  dvrelog3  42098  redvmptabs  42393  reopn  45330  ioontr  45551  iocopn  45560  icoopn  45565  limciccioolb  45661  limcicciooub  45675  lptre2pt  45678  limcresiooub  45680  limcresioolb  45681  limclner  45689  limclr  45693  icccncfext  45925  cncfiooicclem1  45931  fperdvper  45957  stoweidlem53  46091  stoweidlem57  46095  dirkercncflem2  46142  dirkercncflem3  46143  dirkercncflem4  46144  fourierdlem32  46177  fourierdlem33  46178  fourierdlem42  46187  fourierdlem48  46192  fourierdlem49  46193  fourierdlem58  46202  fourierdlem62  46206  fourierdlem73  46217  fouriersw  46269  iooborel  46389  bor1sal  46393  incsmf  46780  decsmf  46805  smfpimbor1lem2  46837  smf2id  46839  smfco  46840  iooii  48949