Theorem uniretop 23479

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

Syntax hints:   = wceq 1539   ∈ wcel 2112  ∪ cuni 4802  ran crn 5530  ‘cfv 6341  ℝcr 10588  (,)cioo 12793  topGenctg 16784  TopBasesctb 21660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-pre-lttri 10663  ax-pre-lttrn 10664

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7160  df-oprab 7161  df-mpo 7162  df-1st 7700  df-2nd 7701  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-ioo 12797  df-topgen 16790  df-bases 21661

This theorem is referenced by:  retopon  23480  retps  23481  icccld  23483  icopnfcld  23484  iocmnfcld  23485  qdensere  23486  zcld  23529  iccntr  23537  icccmp  23541  retopconn  23545  opnreen  23547  rectbntr0  23548  cnmpopc  23644  evth  23675  evth2  23676  evthicc  24174  ovolicc2  24237  opnmbllem  24316  lhop  24730  dvcnvrelem2  24732  dvcnvre  24733  ftc1  24756  taylthlem2  25083  ipasslem8  28734  circtopn  31322  tpr2rico  31397  rrhf  31481  rrhqima  31497  rrhre  31504  brsigarn  31685  unibrsiga  31687  sxbrsigalem3  31772  dya2iocucvr  31784  sxbrsigalem1  31785  orrvcval4  31964  orrvcoel  31965  orrvccel  31966  retopsconn  32741  cvmliftlem10  32786  ivthALT  34109  ptrecube  35373  poimirlem29  35402  poimirlem30  35403  poimirlem31  35404  opnmbllem0  35409  mblfinlem1  35410  mblfinlem2  35411  mblfinlem3  35412  mblfinlem4  35413  ismblfin  35414  ftc1cnnc  35445  refsum2cnlem1  42085  sncldre  42095  reopn  42334  ioontr  42560  limciccioolb  42675  limcicciooub  42691  lptre2pt  42694  limclner  42705  limclr  42709  cncfiooicclem1  42947  fperdvper  42973  itgsubsticclem  43029  stoweidlem62  43116  dirkercncflem2  43158  dirkercncflem3  43159  dirkercncflem4  43160  fourierdlem42  43203  fourierdlem58  43218  fourierdlem73  43233  fouriercnp  43280  fouriercn  43286  cnfsmf  43786  incsmf  43788  decsmf  43812  smfpimbor1lem2  43843