Theorem uniretop 24677

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

Assertion

Ref	Expression
uniretop	⊢ ℝ = ∪ (topGen‘ran (,))

Proof of Theorem uniretop

Step	Hyp	Ref	Expression
1		unirnioo 13349	. 2 ⊢ ℝ = ∪ ran (,)
2		retopbas 24675	. . 3 ⊢ ran (,) ∈ TopBases
3		unitg 22882	. . 3 ⊢ (ran (,) ∈ TopBases → ∪ (topGen‘ran (,)) = ∪ ran (,))
4	2, 3	ax-mp 5	. 2 ⊢ ∪ (topGen‘ran (,)) = ∪ ran (,)
5	1, 4	eqtr4i 2757	1 ⊢ ℝ = ∪ (topGen‘ran (,))

Syntax hints:   = wceq 1541   ∈ wcel 2111  ∪ cuni 4856  ran crn 5615  ‘cfv 6481  ℝcr 11005  (,)cioo 13245  topGenctg 17341  TopBasesctb 22860

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-pre-lttri 11080  ax-pre-lttrn 11081

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-ioo 13249  df-topgen 17347  df-bases 22861

This theorem is referenced by:  retopon  24678  retps  24679  icccld  24681  icopnfcld  24682  iocmnfcld  24683  qdensere  24684  zcld  24729  iccntr  24737  icccmp  24741  retopconn  24745  opnreen  24747  rectbntr0  24748  cnmpopc  24849  evth  24885  evth2  24886  evthicc  25387  ovolicc2  25450  opnmbllem  25529  lhop  25948  dvcnvrelem2  25950  dvcnvre  25951  ftc1  25976  taylthlem2  26309  taylthlem2OLD  26310  ipasslem8  30817  circtopn  33850  tpr2rico  33925  rrhf  34011  rrhqima  34027  rrhre  34034  brsigarn  34197  unibrsiga  34199  sxbrsigalem3  34285  dya2iocucvr  34297  sxbrsigalem1  34298  orrvcval4  34478  orrvcoel  34479  orrvccel  34480  retopsconn  35293  cvmliftlem10  35338  ivthALT  36379  ptrecube  37659  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  ftc1cnnc  37731  readvrec2  42453  refsum2cnlem1  45133  sncldre  45140  reopn  45389  ioontr  45610  limciccioolb  45720  limcicciooub  45734  lptre2pt  45737  limclner  45748  limclr  45752  cncfiooicclem1  45990  fperdvper  46016  itgsubsticclem  46072  stoweidlem62  46159  dirkercncflem2  46201  dirkercncflem3  46202  dirkercncflem4  46203  fourierdlem42  46246  fourierdlem58  46261  fourierdlem73  46276  fouriercnp  46323  fouriercn  46329  cnfsmf  46837  incsmf  46839  decsmf  46864  smfpimbor1lem2  46896