Theorem retop 21792

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

Assertion

Ref	Expression
retop	|- ( topGen ` ran (,) ) e. Top

Proof of Theorem retop

Step	Hyp	Ref	Expression
1		retopbas 21791	. 2 |- ran (,) e. TopBases
2		tgcl 19995	. 2 |- ( ran (,) e. TopBases -> ( topGen ` ran (,) ) e. Top )
3	1, 2	ax-mp 5	1 |- ( topGen ` ran (,) ) e. Top

Syntax hints:   e. wcel 1890   ran crn 4812   ` cfv 5560   (,)cioo 11624   topGenctg 15346   Topctop 19927   TopBasesctb 19930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-pre-lttri 9599  ax-pre-lttrn 9600

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6780  df-2nd 6781  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-ioo 11628  df-topgen 15352  df-top 19931  df-bases 19932

This theorem is referenced by:  retopon  21794  retps  21795  icccld  21797  icopnfcld  21798  iocmnfcld  21799  qdensere  21800  zcld  21841  iccntr  21849  icccmp  21853  reconnlem2  21855  retopcon  21857  rectbntr0  21860  cnmpt2pc  21966  icoopnst  21977  iocopnst  21978  cnheiborlem  21992  bndth  21996  pcoass  22065  evthicc  22420  ovolicc2  22486  subopnmbl  22573  dvlip  22956  dvlip2  22958  dvne0  22974  lhop2  22978  lhop  22979  dvcnvrelem2  22981  dvcnvre  22982  ftc1  23005  taylthlem2  23340  cxpcn3  23699  lgamgulmlem2  23966  circtopn  28670  tpr2rico  28724  rrhqima  28824  rrhre  28831  brsiga  29011  unibrsiga  29014  elmbfmvol2  29094  sxbrsigalem3  29099  dya2iocbrsiga  29102  dya2icobrsiga  29103  dya2iocucvr  29111  sxbrsigalem1  29112  orrvcval4  29302  orrvcoel  29303  orrvccel  29304  retopscon  29977  iccllyscon  29978  rellyscon  29979  cvmliftlem8  30020  cvmliftlem10  30022  ivthALT  30996  ptrecube  31941  poimirlem29  31970  poimirlem30  31971  poimirlem31  31972  poimir  31974  broucube  31975  mblfinlem1  31978  mblfinlem2  31979  mblfinlem3  31980  mblfinlem4  31981  ismblfin  31982  cnambfre  31990  dvtanlemOLD  31992  ftc1cnnc  32017  reopn  37532  ioontr  37651  iocopn  37661  icoopn  37666  limciccioolb  37742  limcicciooub  37758  lptre2pt  37761  limcresiooub  37764  limcresioolb  37765  limclner  37773  limclr  37777  icccncfext  37806  cncfiooicclem1  37812  fperdvper  37831  stoweidlem53  37970  stoweidlem57  37974  stoweidlem59  37976  dirkercncflem2  38022  dirkercncflem3  38023  dirkercncflem4  38024  fourierdlem32  38058  fourierdlem33  38059  fourierdlem42  38068  fourierdlem42OLD  38069  fourierdlem48  38074  fourierdlem49  38075  fourierdlem58  38084  fourierdlem62  38088  fourierdlem73  38099  fouriersw  38151