Theorem retop 24883

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

Syntax hints:   ∈ wcel 2149  ran crn 5660  ‘cfv 6534  (,)cioo 13368  topGenctg 17486  Topctop 23015  TopBasesctb 23067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-pre-lttri 11170  ax-pre-lttrn 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7982  df-2nd 7983  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-ioo 13372  df-topgen 17492  df-top 23016  df-bases 23068

This theorem is referenced by:  retopon  24885  retps  24886  icccld  24888  icopnfcld  24889  iocmnfcld  24890  qdensere  24891  zcld  24936  iccntr  24944  icccmp  24948  reconnlem2  24950  retopconn  24952  rectbntr0  24955  cnmpopc  25052  icoopnst  25063  iocopnst  25064  cnheiborlem  25078  bndth  25082  pcoass  25148  evthicc  25583  ovolicc2  25646  subopnmbl  25728  dvlip  26117  dvlip2  26119  dvne0  26135  lhop2  26139  lhop  26140  dvcnvrelem2  26142  dvcnvre  26143  ftc1  26166  taylthlem2  26499  cxpcn3  26875  lgamgulmlem2  27156  circtopn  34168  tpr2rico  34243  rrhqima  34345  rrhre  34352  brsiga  34514  unibrsiga  34517  elmbfmvol2  34598  sxbrsigalem3  34603  dya2iocbrsiga  34606  dya2icobrsiga  34607  dya2iocucvr  34615  sxbrsigalem1  34616  orrvcval4  34796  orrvcoel  34797  orrvccel  34798  retopsconn  35636  iccllysconn  35637  rellysconn  35638  cvmliftlem8  35679  cvmliftlem10  35681  ivthALT  36731  ptrecube  38154  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  poimir  38187  broucube  38188  mblfinlem1  38191  mblfinlem2  38192  mblfinlem3  38193  mblfinlem4  38194  ismblfin  38195  cnambfre  38202  ftc1cnnc  38226  dvrelog3  42717  redvmptabs  43006  reopn  45895  ioontr  46114  iocopn  46123  icoopn  46128  limciccioolb  46224  limcicciooub  46238  lptre2pt  46241  limcresiooub  46243  limcresioolb  46244  limclner  46252  limclr  46256  icccncfext  46488  cncfiooicclem1  46494  fperdvper  46520  stoweidlem53  46654  stoweidlem57  46658  dirkercncflem2  46705  dirkercncflem3  46706  dirkercncflem4  46707  fourierdlem32  46740  fourierdlem33  46741  fourierdlem42  46750  fourierdlem48  46755  fourierdlem49  46756  fourierdlem58  46765  fourierdlem62  46769  fourierdlem73  46780  fouriersw  46832  iooborel  46952  bor1sal  46956  incsmf  47343  decsmf  47368  smfpimbor1lem2  47400  smf2id  47402  smfco  47403  iooii  49576