Theorem uniretop 24704

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∪ cuni 4861  ran crn 5623  ‘cfv 6490  ℝcr 11023  (,)cioo 13259  topGenctg 17355  TopBasesctb 22887

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-pre-lttri 11098  ax-pre-lttrn 11099

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-ioo 13263  df-topgen 17361  df-bases 22888

This theorem is referenced by:  retopon  24705  retps  24706  icccld  24708  icopnfcld  24709  iocmnfcld  24710  qdensere  24711  zcld  24756  iccntr  24764  icccmp  24768  retopconn  24772  opnreen  24774  rectbntr0  24775  cnmpopc  24876  evth  24912  evth2  24913  evthicc  25414  ovolicc2  25477  opnmbllem  25556  lhop  25975  dvcnvrelem2  25977  dvcnvre  25978  ftc1  26003  taylthlem2  26336  taylthlem2OLD  26337  ipasslem8  30861  circtopn  33943  tpr2rico  34018  rrhf  34104  rrhqima  34120  rrhre  34127  brsigarn  34290  unibrsiga  34292  sxbrsigalem3  34378  dya2iocucvr  34390  sxbrsigalem1  34391  orrvcval4  34571  orrvcoel  34572  orrvccel  34573  retopsconn  35392  cvmliftlem10  35437  ivthALT  36478  ptrecube  37760  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  opnmbllem0  37796  mblfinlem1  37797  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  ftc1cnnc  37832  readvrec2  42558  refsum2cnlem1  45224  sncldre  45231  reopn  45479  ioontr  45699  limciccioolb  45809  limcicciooub  45823  lptre2pt  45826  limclner  45837  limclr  45841  cncfiooicclem1  46079  fperdvper  46105  itgsubsticclem  46161  stoweidlem62  46248  dirkercncflem2  46290  dirkercncflem3  46291  dirkercncflem4  46292  fourierdlem42  46335  fourierdlem58  46350  fourierdlem73  46365  fouriercnp  46412  fouriercn  46418  cnfsmf  46926  incsmf  46928  decsmf  46953  smfpimbor1lem2  46985