Theorem ioossicc 13162

Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)

Assertion

Ref	Expression
ioossicc	⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)

Proof of Theorem ioossicc

Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ioo 13080	. 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2		df-icc 13083	. 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
3		xrltle 12880	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤))
4		xrltle 12880	. 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵))
5	1, 2, 3, 4	ixxssixx 13090	1 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)

Syntax hints:   ⊆ wss 3892  (class class class)co 7269   < clt 11008   ≤ cle 11009  (,)cioo 13076  [,]cicc 13079

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 10926  ax-resscn 10927  ax-pre-lttri 10944  ax-pre-lttrn 10945

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-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-po 5503  df-so 5504  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-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-ov 7272  df-oprab 7273  df-mpo 7274  df-er 8479  df-en 8715  df-dom 8716  df-sdom 8717  df-pnf 11010  df-mnf 11011  df-xr 11012  df-ltxr 11013  df-le 11014  df-ioo 13080  df-icc 13083

This theorem is referenced by:  ioodisj  13211  iccntr  23980  ivth2  24615  ivthle  24616  ivthle2  24617  ovolioo  24728  uniiccvol  24740  itgioo  24976  rollelem  25149  rolle  25150  cmvth  25151  dvlip  25153  dvlipcn  25154  dvlip2  25155  c1liplem1  25156  dvle  25167  dvivthlem1  25168  dvne0  25171  lhop1lem  25173  dvcnvrelem1  25177  dvfsumle  25181  dvfsumge  25182  dvfsumabs  25183  dvfsumlem2  25187  ftc1a  25197  ftc1lem4  25199  ftc1lem5  25200  ftc1lem6  25201  ftc1  25202  ftc2  25204  itgparts  25207  itgsubstlem  25208  itgsubst  25209  itgpowd  25210  reeff1olem  25601  efcvx  25604  cos0pilt1  25684  tanord1  25689  logccv  25814  loglesqrt  25907  chordthm  25983  amgmlem  26135  lgamgulmlem2  26175  eliccioo  31199  xrge0mulc1cn  31885  omssubadd  32261  ftc2re  32572  fdvposlt  32573  fdvneggt  32574  fdvposle  32575  fdvnegge  32576  circlemeth  32614  logdivsqrle  32624  ivthALT  34518  iccioo01  35492  itg2gt0cn  35826  ftc1cnnclem  35842  ftc1cnnc  35843  ftc2nc  35853  areacirc  35864  lcmineqlem10  40041  lcmineqlem12  40043  lhe4.4ex1a  41915  chordthmALT  42521  iccnct  43048  limciccioolb  43131  limcicciooub  43147  icccncfext  43397  cncfiooicclem1  43403  cncfioobdlem  43406  cncfioobd  43407  itgsin0pilem1  43460  iblioosinexp  43463  itgsinexplem1  43464  itgsinexp  43465  ditgeqiooicc  43470  itgcoscmulx  43479  ibliooicc  43481  itgsincmulx  43484  itgsubsticclem  43485  itgioocnicc  43487  iblcncfioo  43488  itgsbtaddcnst  43492  dirkeritg  43612  fourierdlem20  43637  fourierdlem38  43655  fourierdlem39  43656  fourierdlem46  43662  fourierdlem62  43678  fourierdlem68  43684  fourierdlem69  43685  fourierdlem70  43686  fourierdlem72  43688  fourierdlem73  43689  fourierdlem74  43690  fourierdlem75  43691  fourierdlem76  43692  fourierdlem80  43696  fourierdlem81  43697  fourierdlem82  43698  fourierdlem83  43699  fourierdlem84  43700  fourierdlem85  43701  fourierdlem88  43704  fourierdlem92  43708  fourierdlem93  43709  fourierdlem100  43716  fourierdlem101  43717  fourierdlem103  43719  fourierdlem104  43720  fourierdlem107  43723  fourierdlem111  43727  fourierdlem112  43728  sqwvfoura  43738  sqwvfourb  43739  etransclem18  43762  etransclem46  43790  hoicvrrex  44063  iooii  46178