Theorem uniretop 25108

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  ∪ cuni 4870  ran crn 5656  ‘cfv 6555  ℝcr 11223  (,)cioo 13500  topGenctg 17634  TopBasesctb 23290

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-pre-lttri 11298  ax-pre-lttrn 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-1st 8022  df-2nd 8023  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-ioo 13504  df-topgen 17640  df-bases 23291

This theorem is used by:  retopon  25109  retps  25110  icccld  25112  icopnfcld  25113  iocmnfcld  25114  qdensere  25115  zcld  25160  iccntr  25168  icccmp  25172  retopconn  25176  opnreen  25178  rectbntr0  25179  cnmpopc  25276  evth  25307  evth2  25308  evthicc  25807  ovolicc2  25870  opnmbllem  25949  lhop  26363  dvcnvrelem2  26365  dvcnvre  26366  ftc1  26389  taylthlem2  26728  ipasslem8  31466  circtopn  34536  tpr2rico  34611  rrhf  34697  rrhqima  34713  rrhre  34720  brsigarn  34884  unibrsiga  34886  sxbrsigalem3  34971  dya2iocucvr  34983  sxbrsigalem1  34984  orrvcval4  35164  orrvcoel  35165  orrvccel  35166  retopsconn  36180  cvmliftlem10  36225  ivthALT  37300  ptrecube  38729  poimirlem29  38758  poimirlem30  38759  poimirlem31  38760  opnmbllem0  38765  mblfinlem1  38766  mblfinlem2  38767  mblfinlem3  38768  mblfinlem4  38769  ismblfin  38770  ftc1cnnc  38801  readvrec2  43603  refsum2cnlem1  46257  sncldre  46264  reopn  46508  ioontr  46726  limciccioolb  46836  limcicciooub  46850  lptre2pt  46853  limclner  46864  limclr  46868  cncfiooicclem1  47106  fperdvper  47132  itgsubsticclem  47188  stoweidlem62  47275  dirkercncflem2  47317  dirkercncflem3  47318  dirkercncflem4  47319  fourierdlem42  47362  fourierdlem58  47377  fourierdlem73  47392  fouriercnp  47439  fouriercn  47445  cnfsmf  47953  incsmf  47955  decsmf  47980  smfpimbor1lem2  48012