Theorem retopon 25088

Description: The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)

Assertion

Ref	Expression
retopon	⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)

Proof of Theorem retopon

Step	Hyp	Ref	Expression
1		retop 25086	. 2 ⊢ (topGen‘ran (,)) ∈ Top
2		uniretop 25087	. . 3 ⊢ ℝ = ∪ (topGen‘ran (,))
3	2	toptopon 23241	. 2 ⊢ ((topGen‘ran (,)) ∈ Top ↔ (topGen‘ran (,)) ∈ (TopOn‘ℝ))
4	1, 3	mpbi 233	1 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)

This proof depends on syntax axioms:   ∈ wcel 2144  ran crn 5651  ‘cfv 6539  ℝcr 11203  (,)cioo 13480  topGenctg 17614  Topctop 23217  TopOnctopon 23234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-pre-lttri 11278  ax-pre-lttrn 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-oprab 7425  df-mpo 7426  df-1st 8002  df-2nd 8003  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-ioo 13484  df-topgen 17620  df-top 23218  df-topon 23235  df-bases 23270

This theorem is used by:  xrtgioo  25132  reconnlem1  25152  reconn  25154  cnmpopc  25255  cnrehmeo  25280  bndth  25285  evth2  25287  htpycc  25307  pcocn  25344  pcohtpylem  25346  pcopt  25349  pcopt2  25350  pcoass  25351  pcorevlem  25353  circcn  34517  tpr2tp  34583  sxbrsiga  34969  cvmliftlem8  36144  knoppcnlem10  37461  knoppcnlem11  37462  poimir  38665  broucube  38666  cnambfre  38680  reheibor  38867  rfcnpre1  46130  fcnre  46136  refsumcn  46141  refsum2cnlem1  46148  climreeq  46719  islptre  46725  icccncfext  46991  stoweidlem47  47151  dirkercncflem4  47210  dirkercncf  47211  fourierdlem62  47272