Theorem iooretop 23919

Description: Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.)

Assertion

Ref	Expression
iooretop	⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))

Proof of Theorem iooretop

Step	Hyp	Ref	Expression
1		retopbas 23914	. . 3 ⊢ ran (,) ∈ TopBases
2		bastg 22106	. . 3 ⊢ (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
3	1, 2	ax-mp 5	. 2 ⊢ ran (,) ⊆ (topGen‘ran (,))
4		ioorebas 13174	. 2 ⊢ (𝐴(,)𝐵) ∈ ran (,)
5	3, 4	sselii 3923	1 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))

Syntax hints:   ∈ wcel 2110   ⊆ wss 3892  ran crn 5590  ‘cfv 6431  (class class class)co 7269  (,)cioo 13070  topGenctg 17138  TopBasesctb 22085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-cnex 10920  ax-resscn 10921  ax-1cn 10922  ax-icn 10923  ax-addcl 10924  ax-addrcl 10925  ax-mulcl 10926  ax-mulrcl 10927  ax-mulcom 10928  ax-addass 10929  ax-mulass 10930  ax-distr 10931  ax-i2m1 10932  ax-1ne0 10933  ax-1rid 10934  ax-rnegex 10935  ax-rrecex 10936  ax-cnre 10937  ax-pre-lttri 10938  ax-pre-lttrn 10939  ax-pre-ltadd 10940  ax-pre-mulgt0 10941  ax-pre-sup 10942

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7702  df-1st 7818  df-2nd 7819  df-frecs 8082  df-wrecs 8113  df-recs 8187  df-rdg 8226  df-er 8473  df-en 8709  df-dom 8710  df-sdom 8711  df-sup 9171  df-inf 9172  df-pnf 11004  df-mnf 11005  df-xr 11006  df-ltxr 11007  df-le 11008  df-sub 11199  df-neg 11200  df-div 11625  df-nn 11966  df-n0 12226  df-z 12312  df-uz 12574  df-q 12680  df-ioo 13074  df-topgen 17144  df-bases 22086

This theorem is referenced by:  icccld  23920  icopnfcld  23921  iocmnfcld  23922  zcld  23966  iccntr  23974  reconnlem1  23979  reconnlem2  23980  icoopnst  24092  iocopnst  24093  dvlip  25147  dvlipcn  25148  dvivthlem1  25162  dvne0  25165  lhop2  25169  lhop  25170  dvfsumle  25175  dvfsumabs  25177  dvfsumlem2  25181  ftc1  25196  dvloglem  25793  advlog  25799  advlogexp  25800  cxpcn3  25891  loglesqrt  25901  lgamgulmlem2  26169  log2sumbnd  26682  dya2iocbrsiga  32230  dya2icobrsiga  32231  poimir  35798  ftc1cnnc  35837  areacirclem1  35853  dvrelog3  40062  aks4d1p1p6  40070  rfcnpre1  42524  rfcnpre2  42536  ioontr  43012  iocopn  43021  icoopn  43026  islptre  43123  limciccioolb  43125  limcicciooub  43141  limcresiooub  43146  limcresioolb  43147  icccncfext  43391  itgsin0pilem1  43454  itgsbtaddcnst  43486  dirkercncflem2  43608  dirkercncflem3  43609  dirkercncflem4  43610  fourierdlem28  43639  fourierdlem32  43643  fourierdlem33  43644  fourierdlem48  43658  fourierdlem49  43659  fourierdlem56  43666  fourierdlem57  43667  fourierdlem59  43669  fourierdlem60  43670  fourierdlem61  43671  fourierdlem62  43672  fourierdlem68  43678  fourierdlem72  43682  fourierdlem73  43683  fouriersw  43735  iooborel  43853  iooii  46172  i0oii  46174  io1ii  46175