Theorem icossicc 13387

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

Syntax hints:   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3890   class class class wbr 5079  (class class class)co 7363  ℝ^*cxr 11176   < clt 11177   ≤ cle 11178  [,)cico 13298  [,]cicc 13299

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-pre-lttri 11110  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-ico 13302  df-icc 13303

This theorem is referenced by:  iccpnfcnv  24936  itg2mulclem  25738  itg2mulc  25739  itg2monolem1  25742  itg2monolem2  25743  itg2monolem3  25744  itg2mono  25745  itg2i1fseq3  25749  itg2addlem  25750  itg2gt0  25752  itg2cnlem2  25754  psercnlem2  26414  eliccelico  32876  xrge0slmod  33438  xrge0iifcnv  34124  lmlimxrge0  34139  lmdvglim  34145  esumfsupre  34262  esumpfinvallem  34265  esumpfinval  34266  esumpfinvalf  34267  esumpcvgval  34269  esumpmono  34270  esummulc1  34272  sitmcl  34542  itg2addnc  38048  itg2gt0cn  38049  ftc1anclem6  38072  ftc1anclem8  38074  icoiccdif  45976  limciccioolb  46073  ltmod  46088  fourierdlem63  46619  fge0icoicc  46815  sge0tsms  46830  sge0iunmptlemre  46865  sge0isum  46877  sge0xaddlem1  46883  sge0xaddlem2  46884  sge0pnffsumgt  46892  sge0gtfsumgt  46893  sge0seq  46896  ovnsupge0  47007  ovnlecvr  47008  ovnsubaddlem1  47020  sge0hsphoire  47039  hoidmv1lelem3  47043  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoidmvlelem5  47049  hoidmvle  47050  ovnhoilem1  47051  ovnlecvr2  47060  hspmbllem2  47077  sepfsepc  49425