Theorem icossicc 13340

Description: A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)

Assertion

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

Proof of Theorem icossicc

Dummy variables 𝑎 𝑏 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ico 13255	. 2 ⊢ [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 < 𝑏)})
2		df-icc 13256	. 2 ⊢ [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 ≤ 𝑏)})
3		idd 24	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 ≤ 𝑤 → 𝐴 ≤ 𝑤))
4		xrltle 13052	. 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵))
5	1, 2, 3, 4	ixxssixx 13263	1 ⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3898   class class class wbr 5095  (class class class)co 7354  ℝ^*cxr 11154   < clt 11155   ≤ cle 11156  [,)cico 13251  [,]cicc 13252

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-cnex 11071  ax-resscn 11072  ax-pre-lttri 11089  ax-pre-lttrn 11090

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7357  df-oprab 7358  df-mpo 7359  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-ico 13255  df-icc 13256

This theorem is referenced by:  iccpnfcnv  24872  itg2mulclem  25677  itg2mulc  25678  itg2monolem1  25681  itg2monolem2  25682  itg2monolem3  25683  itg2mono  25684  itg2i1fseq3  25688  itg2addlem  25689  itg2gt0  25691  itg2cnlem2  25693  psercnlem2  26364  eliccelico  32766  xrge0slmod  33322  xrge0iifcnv  33969  lmlimxrge0  33984  lmdvglim  33990  esumfsupre  34107  esumpfinvallem  34110  esumpfinval  34111  esumpfinvalf  34112  esumpcvgval  34114  esumpmono  34115  esummulc1  34117  sitmcl  34387  itg2addnc  37737  itg2gt0cn  37738  ftc1anclem6  37761  ftc1anclem8  37763  icoiccdif  45651  limciccioolb  45748  ltmod  45763  fourierdlem63  46294  fge0icoicc  46490  sge0tsms  46505  sge0iunmptlemre  46540  sge0isum  46552  sge0xaddlem1  46558  sge0xaddlem2  46559  sge0pnffsumgt  46567  sge0gtfsumgt  46568  sge0seq  46571  ovnsupge0  46682  ovnlecvr  46683  ovnsubaddlem1  46695  sge0hsphoire  46714  hoidmv1lelem3  46718  hoidmv1le  46719  hoidmvlelem1  46720  hoidmvlelem2  46721  hoidmvlelem3  46722  hoidmvlelem4  46723  hoidmvlelem5  46724  hoidmvle  46725  ovnhoilem1  46726  ovnlecvr2  46735  hspmbllem2  46752  sepfsepc  49055