Theorem icossicc 13433

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 13348	. 2 ⊢ [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 < 𝑏)})
2		df-icc 13349	. 2 ⊢ [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 ≤ 𝑏)})
3		idd 24	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 ≤ 𝑤 → 𝐴 ≤ 𝑤))
4		xrltle 13144	. 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵))
5	1, 2, 3, 4	ixxssixx 13356	1 ⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)

Syntax hints:   ∧ wa 399   ∈ wcel 2141   ⊆ wss 3902   class class class wbr 5097  (class class class)co 7390  ℝ^*cxr 11208   < clt 11209   ≤ cle 11210  [,)cico 13344  [,]cicc 13345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-pre-lttri 11140  ax-pre-lttrn 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-ico 13348  df-icc 13349

This theorem is referenced by:  iccpnfcnv  24993  itg2mulclem  25795  itg2mulc  25796  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2i1fseq3  25806  itg2addlem  25807  itg2gt0  25809  itg2cnlem2  25811  psercnlem2  26474  eliccelico  32939  xrge0slmod  33494  xrge0iifcnv  34190  lmlimxrge0  34205  lmdvglim  34211  esumfsupre  34328  esumpfinvallem  34331  esumpfinval  34332  esumpfinvalf  34333  esumpcvgval  34335  esumpmono  34336  esummulc1  34338  sitmcl  34608  itg2addnc  38133  itg2gt0cn  38134  ftc1anclem6  38157  ftc1anclem8  38159  icoiccdif  46060  limciccioolb  46157  ltmod  46172  fourierdlem63  46703  fge0icoicc  46899  sge0tsms  46914  sge0iunmptlemre  46949  sge0isum  46961  sge0xaddlem1  46967  sge0xaddlem2  46968  sge0pnffsumgt  46976  sge0gtfsumgt  46977  sge0seq  46980  ovnsupge0  47091  ovnlecvr  47092  ovnsubaddlem1  47104  sge0hsphoire  47123  hoidmv1lelem3  47127  hoidmv1le  47128  hoidmvlelem1  47129  hoidmvlelem2  47130  hoidmvlelem3  47131  hoidmvlelem4  47132  hoidmvlelem5  47133  hoidmvle  47134  ovnhoilem1  47135  ovnlecvr2  47144  hspmbllem2  47161  sepfsepc  49509