MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  icossicc Structured version   Visualization version   GIF version

Theorem icossicc 12451
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.
StepHypRef Expression
1 df-ico 12372 . 2 [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎𝑥𝑥 < 𝑏)})
2 df-icc 12373 . 2 [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎𝑥𝑥𝑏)})
3 idd 24 . 2 ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐴𝑤𝐴𝑤))
4 xrltle 12173 . 2 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑤 < 𝐵𝑤𝐵))
51, 2, 3, 4ixxssixx 12380 1 (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 2137  wss 3713   class class class wbr 4802  (class class class)co 6811  *cxr 10263   < clt 10264  cle 10265  [,)cico 12368  [,]cicc 12369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-pre-lttri 10200  ax-pre-lttrn 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-ico 12372  df-icc 12373
This theorem is referenced by:  iccpnfcnv  22942  itg2mulclem  23710  itg2mulc  23711  itg2monolem1  23714  itg2monolem2  23715  itg2monolem3  23716  itg2mono  23717  itg2i1fseqle  23718  itg2i1fseq3  23721  itg2addlem  23722  itg2gt0  23724  itg2cnlem2  23726  psercnlem2  24375  eliccelico  29846  xrge0slmod  30151  xrge0iifcnv  30286  lmlimxrge0  30301  lmdvglim  30307  esumfsupre  30440  esumpfinvallem  30443  esumpfinval  30444  esumpfinvalf  30445  esumpcvgval  30447  esumpmono  30448  esummulc1  30450  sitmcl  30720  itg2addnc  33775  itg2gt0cn  33776  ftc1anclem6  33801  ftc1anclem8  33803  icoiccdif  40251  limciccioolb  40354  ltmod  40371  fourierdlem63  40887  fge0icoicc  41083  sge0tsms  41098  sge0iunmptlemre  41133  sge0isum  41145  sge0xaddlem1  41151  sge0xaddlem2  41152  sge0pnffsumgt  41160  sge0gtfsumgt  41161  sge0seq  41164  ovnsupge0  41275  ovnlecvr  41276  ovnsubaddlem1  41288  sge0hsphoire  41307  hoidmv1lelem3  41311  hoidmv1le  41312  hoidmvlelem1  41313  hoidmvlelem2  41314  hoidmvlelem3  41315  hoidmvlelem4  41316  hoidmvlelem5  41317  hoidmvle  41318  ovnhoilem1  41319  ovnlecvr2  41328  hspmbllem2  41345
  Copyright terms: Public domain W3C validator