Theorem ioossicc 13415

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 13333	. 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2		df-icc 13336	. 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
3		xrltle 13133	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤))
4		xrltle 13133	. 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵))
5	1, 2, 3, 4	ixxssixx 13343	1 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)

Syntax hints:   ⊆ wss 3948  (class class class)co 7412   < clt 11253   ≤ cle 11254  (,)cioo 13329  [,]cicc 13332

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-pre-lttri 11188  ax-pre-lttrn 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-ioo 13333  df-icc 13336

This theorem is referenced by:  ioodisj  13464  iccntr  24558  ivth2  25205  ivthle  25206  ivthle2  25207  ovolioo  25318  uniiccvol  25330  itgioo  25566  rollelem  25742  rolle  25743  cmvth  25744  dvlip  25746  dvlipcn  25747  dvlip2  25748  c1liplem1  25749  dvle  25760  dvivthlem1  25761  dvne0  25764  lhop1lem  25766  dvcnvrelem1  25770  dvfsumle  25774  dvfsumge  25775  dvfsumabs  25776  dvfsumlem2  25780  ftc1a  25790  ftc1lem4  25792  ftc1lem5  25793  ftc1lem6  25794  ftc1  25795  ftc2  25797  itgparts  25800  itgsubstlem  25801  itgsubst  25802  itgpowd  25803  reeff1olem  26195  efcvx  26198  cos0pilt1  26278  tanord1  26283  logccv  26408  loglesqrt  26503  chordthm  26579  amgmlem  26731  lgamgulmlem2  26771  eliccioo  32365  xrge0mulc1cn  33220  omssubadd  33598  ftc2re  33909  fdvposlt  33910  fdvneggt  33911  fdvposle  33912  fdvnegge  33913  circlemeth  33951  logdivsqrle  33961  gg-cmvth  35467  gg-dvfsumle  35469  gg-dvfsumlem2  35470  ivthALT  35524  iccioo01  36512  itg2gt0cn  36847  ftc1cnnclem  36863  ftc1cnnc  36864  ftc2nc  36874  areacirc  36885  lcmineqlem10  41210  lcmineqlem12  41212  lhe4.4ex1a  43391  chordthmALT  43997  iccnct  44553  limciccioolb  44636  limcicciooub  44652  icccncfext  44902  cncfiooicclem1  44908  cncfioobdlem  44911  cncfioobd  44912  itgsin0pilem1  44965  iblioosinexp  44968  itgsinexplem1  44969  itgsinexp  44970  ditgeqiooicc  44975  itgcoscmulx  44984  ibliooicc  44986  itgsincmulx  44989  itgsubsticclem  44990  itgioocnicc  44992  iblcncfioo  44993  itgsbtaddcnst  44997  dirkeritg  45117  fourierdlem20  45142  fourierdlem38  45160  fourierdlem39  45161  fourierdlem46  45167  fourierdlem62  45183  fourierdlem68  45189  fourierdlem69  45190  fourierdlem70  45191  fourierdlem72  45193  fourierdlem73  45194  fourierdlem74  45195  fourierdlem75  45196  fourierdlem76  45197  fourierdlem80  45201  fourierdlem81  45202  fourierdlem82  45203  fourierdlem83  45204  fourierdlem84  45205  fourierdlem85  45206  fourierdlem88  45209  fourierdlem92  45213  fourierdlem93  45214  fourierdlem100  45221  fourierdlem101  45222  fourierdlem103  45224  fourierdlem104  45225  fourierdlem107  45228  fourierdlem111  45232  fourierdlem112  45233  sqwvfoura  45243  sqwvfourb  45244  etransclem18  45267  etransclem46  45295  hoicvrrex  45571  iooii  47638