Theorem retop 23058

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

Syntax hints:   ∈ wcel 2081  ran crn 5449  ‘cfv 6230  (,)cioo 12593  topGenctg 16545  Topctop 21190  TopBasesctb 21242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-cnex 10444  ax-resscn 10445  ax-pre-lttri 10462  ax-pre-lttrn 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-po 5367  df-so 5368  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-1st 7550  df-2nd 7551  df-er 8144  df-en 8363  df-dom 8364  df-sdom 8365  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-ioo 12597  df-topgen 16551  df-top 21191  df-bases 21243

This theorem is referenced by:  retopon  23060  retps  23061  icccld  23063  icopnfcld  23064  iocmnfcld  23065  qdensere  23066  zcld  23109  iccntr  23117  icccmp  23121  reconnlem2  23123  retopconn  23125  rectbntr0  23128  cnmpopc  23220  icoopnst  23231  iocopnst  23232  cnheiborlem  23246  bndth  23250  pcoass  23316  evthicc  23748  ovolicc2  23811  subopnmbl  23893  dvlip  24278  dvlip2  24280  dvne0  24296  lhop2  24300  lhop  24301  dvcnvrelem2  24303  dvcnvre  24304  ftc1  24327  taylthlem2  24650  cxpcn3  25015  lgamgulmlem2  25294  circtopn  30723  tpr2rico  30777  rrhqima  30877  rrhre  30884  brsiga  31064  unibrsiga  31067  elmbfmvol2  31147  sxbrsigalem3  31152  dya2iocbrsiga  31155  dya2icobrsiga  31156  dya2iocucvr  31164  sxbrsigalem1  31165  orrvcval4  31344  orrvcoel  31345  orrvccel  31346  retopsconn  32111  iccllysconn  32112  rellysconn  32113  cvmliftlem8  32154  cvmliftlem10  32156  ivthALT  33299  ptrecube  34449  poimirlem29  34478  poimirlem30  34479  poimirlem31  34480  poimir  34482  broucube  34483  mblfinlem1  34486  mblfinlem2  34487  mblfinlem3  34488  mblfinlem4  34489  ismblfin  34490  cnambfre  34497  ftc1cnnc  34523  reopn  41122  ioontr  41355  iocopn  41364  icoopn  41369  limciccioolb  41470  limcicciooub  41486  lptre2pt  41489  limcresiooub  41491  limcresioolb  41492  limclner  41500  limclr  41504  icccncfext  41738  cncfiooicclem1  41744  fperdvper  41771  stoweidlem53  41907  stoweidlem57  41911  dirkercncflem2  41958  dirkercncflem3  41959  dirkercncflem4  41960  fourierdlem32  41993  fourierdlem33  41994  fourierdlem42  42003  fourierdlem48  42008  fourierdlem49  42009  fourierdlem58  42018  fourierdlem62  42022  fourierdlem73  42033  fouriersw  42085  iooborel  42203  bor1sal  42207  incsmf  42588  decsmf  42612  smfpimbor1lem2  42643  smf2id  42645  smfco  42646