Theorem retop 22785

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

Syntax hints:   ∈ wcel 2145  ran crn 5250  ‘cfv 6031  (,)cioo 12380  topGenctg 16306  Topctop 20918  TopBasesctb 20970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-pre-lttri 10212  ax-pre-lttrn 10213

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-1st 7315  df-2nd 7316  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-ioo 12384  df-topgen 16312  df-top 20919  df-bases 20971

This theorem is referenced by:  retopon  22787  retps  22788  icccld  22790  icopnfcld  22791  iocmnfcld  22792  qdensere  22793  zcld  22836  iccntr  22844  icccmp  22848  reconnlem2  22850  retopconn  22852  rectbntr0  22855  cnmpt2pc  22947  icoopnst  22958  iocopnst  22959  cnheiborlem  22973  bndth  22977  pcoass  23043  evthicc  23447  ovolicc2  23510  subopnmbl  23592  dvlip  23976  dvlip2  23978  dvne0  23994  lhop2  23998  lhop  23999  dvcnvrelem2  24001  dvcnvre  24002  ftc1  24025  taylthlem2  24348  cxpcn3  24710  lgamgulmlem2  24977  circtopn  30244  tpr2rico  30298  rrhqima  30398  rrhre  30405  brsiga  30586  unibrsiga  30589  elmbfmvol2  30669  sxbrsigalem3  30674  dya2iocbrsiga  30677  dya2icobrsiga  30678  dya2iocucvr  30686  sxbrsigalem1  30687  orrvcval4  30866  orrvcoel  30867  orrvccel  30868  retopsconn  31569  iccllysconn  31570  rellysconn  31571  cvmliftlem8  31612  cvmliftlem10  31614  ivthALT  32667  ptrecube  33742  poimirlem29  33771  poimirlem30  33772  poimirlem31  33773  poimir  33775  broucube  33776  mblfinlem1  33779  mblfinlem2  33780  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  cnambfre  33790  ftc1cnnc  33816  reopn  40019  ioontr  40256  iocopn  40265  icoopn  40270  limciccioolb  40371  limcicciooub  40387  lptre2pt  40390  limcresiooub  40392  limcresioolb  40393  limclner  40401  limclr  40405  icccncfext  40618  cncfiooicclem1  40624  fperdvper  40651  stoweidlem53  40787  stoweidlem57  40791  dirkercncflem2  40838  dirkercncflem3  40839  dirkercncflem4  40840  fourierdlem32  40873  fourierdlem33  40874  fourierdlem42  40883  fourierdlem48  40888  fourierdlem49  40889  fourierdlem58  40898  fourierdlem62  40902  fourierdlem73  40913  fouriersw  40965  iooborel  41086  bor1sal  41090  incsmf  41471  decsmf  41495  smfpimbor1lem2  41526  smf2id  41528  smfco  41529