Theorem retop 24705

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

Syntax hints:   ∈ wcel 2113  ran crn 5625  ‘cfv 6492  (,)cioo 13261  topGenctg 17357  Topctop 22837  TopBasesctb 22889

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-pre-lttri 11100  ax-pre-lttrn 11101

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-ioo 13265  df-topgen 17363  df-top 22838  df-bases 22890

This theorem is referenced by:  retopon  24707  retps  24708  icccld  24710  icopnfcld  24711  iocmnfcld  24712  qdensere  24713  zcld  24758  iccntr  24766  icccmp  24770  reconnlem2  24772  retopconn  24774  rectbntr0  24777  cnmpopc  24878  icoopnst  24892  iocopnst  24893  cnheiborlem  24909  bndth  24913  pcoass  24980  evthicc  25416  ovolicc2  25479  subopnmbl  25561  dvlip  25954  dvlip2  25956  dvne0  25972  lhop2  25976  lhop  25977  dvcnvrelem2  25979  dvcnvre  25980  ftc1  26005  taylthlem2  26338  taylthlem2OLD  26339  cxpcn3  26714  lgamgulmlem2  26996  circtopn  33994  tpr2rico  34069  rrhqima  34171  rrhre  34178  brsiga  34340  unibrsiga  34343  elmbfmvol2  34424  sxbrsigalem3  34429  dya2iocbrsiga  34432  dya2icobrsiga  34433  dya2iocucvr  34441  sxbrsigalem1  34442  orrvcval4  34622  orrvcoel  34623  orrvccel  34624  retopsconn  35443  iccllysconn  35444  rellysconn  35445  cvmliftlem8  35486  cvmliftlem10  35488  ivthALT  36529  ptrecube  37821  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimir  37854  broucube  37855  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  cnambfre  37869  ftc1cnnc  37893  dvrelog3  42319  redvmptabs  42615  reopn  45537  ioontr  45757  iocopn  45766  icoopn  45771  limciccioolb  45867  limcicciooub  45881  lptre2pt  45884  limcresiooub  45886  limcresioolb  45887  limclner  45895  limclr  45899  icccncfext  46131  cncfiooicclem1  46137  fperdvper  46163  stoweidlem53  46297  stoweidlem57  46301  dirkercncflem2  46348  dirkercncflem3  46349  dirkercncflem4  46350  fourierdlem32  46383  fourierdlem33  46384  fourierdlem42  46393  fourierdlem48  46398  fourierdlem49  46399  fourierdlem58  46408  fourierdlem62  46412  fourierdlem73  46423  fouriersw  46475  iooborel  46595  bor1sal  46599  incsmf  46986  decsmf  47011  smfpimbor1lem2  47043  smf2id  47045  smfco  47046  iooii  49163