Theorem retopon 24707

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 24705	. 2 ⊢ (topGen‘ran (,)) ∈ Top
2		uniretop 24706	. . 3 ⊢ ℝ = ∪ (topGen‘ran (,))
3	2	toptopon 22861	. 2 ⊢ ((topGen‘ran (,)) ∈ Top ↔ (topGen‘ran (,)) ∈ (TopOn‘ℝ))
4	1, 3	mpbi 230	1 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)

Syntax hints:   ∈ wcel 2113  ran crn 5625  ‘cfv 6492  ℝcr 11025  (,)cioo 13261  topGenctg 17357  Topctop 22837  TopOnctopon 22854

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-pre-lttri 11100  ax-pre-lttrn 11101

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-ioo 13265  df-topgen 17363  df-top 22838  df-topon 22855  df-bases 22890

This theorem is referenced by:  xrtgioo  24751  reconnlem1  24771  reconn  24773  cnmpopc  24878  cnrehmeo  24907  cnrehmeoOLD  24908  bndth  24913  evth2  24915  htpycc  24935  pcocn  24973  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  circcn  33995  tpr2tp  34061  sxbrsiga  34447  cvmliftlem8  35486  knoppcnlem10  36702  knoppcnlem11  36703  poimir  37854  broucube  37855  cnambfre  37869  reheibor  38040  rfcnpre1  45264  fcnre  45270  refsumcn  45275  refsum2cnlem1  45282  climreeq  45859  islptre  45865  icccncfext  46131  stoweidlem47  46291  dirkercncflem4  46350  dirkercncf  46351  fourierdlem62  46412