Theorem uniretop 24699

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∪ cuni 4883  ran crn 5655  ‘cfv 6530  ℝcr 11126  (,)cioo 13360  topGenctg 17449  TopBasesctb 22881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-1st 7986  df-2nd 7987  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-ioo 13364  df-topgen 17455  df-bases 22882

This theorem is referenced by:  retopon  24700  retps  24701  icccld  24703  icopnfcld  24704  iocmnfcld  24705  qdensere  24706  zcld  24751  iccntr  24759  icccmp  24763  retopconn  24767  opnreen  24769  rectbntr0  24770  cnmpopc  24871  evth  24907  evth2  24908  evthicc  25410  ovolicc2  25473  opnmbllem  25552  lhop  25971  dvcnvrelem2  25973  dvcnvre  25974  ftc1  25999  taylthlem2  26332  taylthlem2OLD  26333  ipasslem8  30764  circtopn  33814  tpr2rico  33889  rrhf  33975  rrhqima  33991  rrhre  33998  brsigarn  34161  unibrsiga  34163  sxbrsigalem3  34250  dya2iocucvr  34262  sxbrsigalem1  34263  orrvcval4  34443  orrvcoel  34444  orrvccel  34445  retopsconn  35217  cvmliftlem10  35262  ivthALT  36299  ptrecube  37590  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  ftc1cnnc  37662  readvrec2  42351  refsum2cnlem1  45009  sncldre  45016  reopn  45266  ioontr  45488  limciccioolb  45598  limcicciooub  45614  lptre2pt  45617  limclner  45628  limclr  45632  cncfiooicclem1  45870  fperdvper  45896  itgsubsticclem  45952  stoweidlem62  46039  dirkercncflem2  46081  dirkercncflem3  46082  dirkercncflem4  46083  fourierdlem42  46126  fourierdlem58  46141  fourierdlem73  46156  fouriercnp  46203  fouriercn  46209  cnfsmf  46717  incsmf  46719  decsmf  46744  smfpimbor1lem2  46776