Theorem ioossicc 12464

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

Syntax hints:   ⊆ wss 3723  (class class class)co 6793   < clt 10276   ≤ cle 10277  (,)cioo 12380  [,]cicc 12383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-pre-lttri 10212  ax-pre-lttrn 10213

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-ioo 12384  df-icc 12387

This theorem is referenced by:  ioodisj  12509  iccntr  22844  ivth2  23443  ivthle  23444  ivthle2  23445  ovolioo  23556  uniiccvol  23568  itgioo  23802  rollelem  23972  rolle  23973  cmvth  23974  dvlip  23976  dvlipcn  23977  dvlip2  23978  c1liplem1  23979  dvle  23990  dvivthlem1  23991  dvne0  23994  lhop1lem  23996  dvcnvrelem1  24000  dvfsumle  24004  dvfsumge  24005  dvfsumabs  24006  dvfsumlem2  24010  ftc1a  24020  ftc1lem4  24022  ftc1lem5  24023  ftc1lem6  24024  ftc1  24025  ftc2  24027  itgparts  24030  itgsubstlem  24031  itgsubst  24032  reeff1olem  24420  efcvx  24423  tanord1  24504  logccv  24630  loglesqrt  24720  chordthm  24785  amgmlem  24937  lgamgulmlem2  24977  eliccioo  29979  xrge0mulc1cn  30327  omssubadd  30702  ftc2re  31016  fdvposlt  31017  fdvneggt  31018  fdvposle  31019  fdvnegge  31020  circlemeth  31058  logdivsqrle  31068  ivthALT  32667  itg2gt0cn  33797  ftc1cnnclem  33815  ftc1cnnc  33816  ftc2nc  33826  areacirc  33837  itgpowd  38326  lhe4.4ex1a  39054  chordthmALT  39691  iccnct  40286  limciccioolb  40371  limcicciooub  40387  icccncfext  40618  cncfiooicclem1  40624  cncfioobdlem  40627  cncfioobd  40628  itgsin0pilem1  40683  iblioosinexp  40686  itgsinexplem1  40687  itgsinexp  40688  ditgeqiooicc  40693  itgcoscmulx  40702  ibliooicc  40704  itgsincmulx  40707  itgsubsticclem  40708  itgioocnicc  40710  iblcncfioo  40711  itgsbtaddcnst  40715  dirkeritg  40836  fourierdlem20  40861  fourierdlem38  40879  fourierdlem39  40880  fourierdlem46  40886  fourierdlem62  40902  fourierdlem68  40908  fourierdlem69  40909  fourierdlem70  40910  fourierdlem72  40912  fourierdlem73  40913  fourierdlem74  40914  fourierdlem75  40915  fourierdlem76  40916  fourierdlem80  40920  fourierdlem81  40921  fourierdlem82  40922  fourierdlem83  40923  fourierdlem84  40924  fourierdlem85  40925  fourierdlem88  40928  fourierdlem92  40932  fourierdlem93  40933  fourierdlem100  40940  fourierdlem101  40941  fourierdlem103  40943  fourierdlem104  40944  fourierdlem107  40947  fourierdlem111  40951  fourierdlem112  40952  sqwvfoura  40962  sqwvfourb  40963  etransclem18  40986  etransclem46  41014  hoicvrrex  41290