Theorem uniretop 24749

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 13397	. 2 ⊢ ℝ = ∪ ran (,)
2		retopbas 24747	. . 3 ⊢ ran (,) ∈ TopBases
3		unitg 22954	. . 3 ⊢ (ran (,) ∈ TopBases → ∪ (topGen‘ran (,)) = ∪ ran (,))
4	2, 3	ax-mp 5	. 2 ⊢ ∪ (topGen‘ran (,)) = ∪ ran (,)
5	1, 4	eqtr4i 2767	1 ⊢ ℝ = ∪ (topGen‘ran (,))

Syntax hints:   = wceq 1548   ∈ wcel 2121  ∪ cuni 4841  ran crn 5622  ‘cfv 6489  ℝcr 11032  (,)cioo 13293  topGenctg 17395  TopBasesctb 22932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107  ax-pre-lttrn 11108

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-ioo 13297  df-topgen 17401  df-bases 22933

This theorem is referenced by:  retopon  24750  retps  24751  icccld  24753  icopnfcld  24754  iocmnfcld  24755  qdensere  24756  zcld  24801  iccntr  24809  icccmp  24813  retopconn  24817  opnreen  24819  rectbntr0  24820  cnmpopc  24917  evth  24948  evth2  24949  evthicc  25448  ovolicc2  25511  opnmbllem  25590  lhop  26005  dvcnvrelem2  26007  dvcnvre  26008  ftc1  26031  taylthlem2  26361  ipasslem8  30930  circtopn  34033  tpr2rico  34108  rrhf  34194  rrhqima  34210  rrhre  34217  brsigarn  34380  unibrsiga  34382  sxbrsigalem3  34468  dya2iocucvr  34480  sxbrsigalem1  34481  orrvcval4  34661  orrvcoel  34662  orrvccel  34663  retopsconn  35492  cvmliftlem10  35537  ivthALT  36578  ptrecube  38002  poimirlem29  38031  poimirlem30  38032  poimirlem31  38033  opnmbllem0  38038  mblfinlem1  38039  mblfinlem2  38040  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  ftc1cnnc  38074  readvrec2  42853  refsum2cnlem1  45500  sncldre  45507  reopn  45751  ioontr  45970  limciccioolb  46080  limcicciooub  46094  lptre2pt  46097  limclner  46108  limclr  46112  cncfiooicclem1  46350  fperdvper  46376  itgsubsticclem  46432  stoweidlem62  46519  dirkercncflem2  46561  dirkercncflem3  46562  dirkercncflem4  46563  fourierdlem42  46606  fourierdlem58  46621  fourierdlem73  46636  fouriercnp  46683  fouriercn  46689  cnfsmf  47197  incsmf  47199  decsmf  47224  smfpimbor1lem2  47256