Theorem retop 23364

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

Syntax hints:   ∈ wcel 2110  ran crn 5551  ‘cfv 6350  (,)cioo 12732  topGenctg 16705  Topctop 21495  TopBasesctb 21547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605  ax-pre-lttrn 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-po 5469  df-so 5470  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-ioo 12736  df-topgen 16711  df-top 21496  df-bases 21548

This theorem is referenced by:  retopon  23366  retps  23367  icccld  23369  icopnfcld  23370  iocmnfcld  23371  qdensere  23372  zcld  23415  iccntr  23423  icccmp  23427  reconnlem2  23429  retopconn  23431  rectbntr0  23434  cnmpopc  23526  icoopnst  23537  iocopnst  23538  cnheiborlem  23552  bndth  23556  pcoass  23622  evthicc  24054  ovolicc2  24117  subopnmbl  24199  dvlip  24584  dvlip2  24586  dvne0  24602  lhop2  24606  lhop  24607  dvcnvrelem2  24609  dvcnvre  24610  ftc1  24633  taylthlem2  24956  cxpcn3  25323  lgamgulmlem2  25601  circtopn  31096  tpr2rico  31150  rrhqima  31250  rrhre  31257  brsiga  31437  unibrsiga  31440  elmbfmvol2  31520  sxbrsigalem3  31525  dya2iocbrsiga  31528  dya2icobrsiga  31529  dya2iocucvr  31537  sxbrsigalem1  31538  orrvcval4  31717  orrvcoel  31718  orrvccel  31719  retopsconn  32491  iccllysconn  32492  rellysconn  32493  cvmliftlem8  32534  cvmliftlem10  32536  ivthALT  33678  ptrecube  34886  poimirlem29  34915  poimirlem30  34916  poimirlem31  34917  poimir  34919  broucube  34920  mblfinlem1  34923  mblfinlem2  34924  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  cnambfre  34934  ftc1cnnc  34960  reopn  41547  ioontr  41779  iocopn  41788  icoopn  41793  limciccioolb  41894  limcicciooub  41910  lptre2pt  41913  limcresiooub  41915  limcresioolb  41916  limclner  41924  limclr  41928  icccncfext  42162  cncfiooicclem1  42168  fperdvper  42195  stoweidlem53  42331  stoweidlem57  42335  dirkercncflem2  42382  dirkercncflem3  42383  dirkercncflem4  42384  fourierdlem32  42417  fourierdlem33  42418  fourierdlem42  42427  fourierdlem48  42432  fourierdlem49  42433  fourierdlem58  42442  fourierdlem62  42446  fourierdlem73  42457  fouriersw  42509  iooborel  42627  bor1sal  42631  incsmf  43012  decsmf  43036  smfpimbor1lem2  43067  smf2id  43069  smfco  43070