![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > icossicc | Structured version Visualization version GIF version |
Description: A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.) |
Ref | Expression |
---|---|
icossicc | ⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ico 12345 | . 2 ⊢ [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 < 𝑏)}) | |
2 | df-icc 12346 | . 2 ⊢ [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 ≤ 𝑏)}) | |
3 | idd 24 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 ≤ 𝑤 → 𝐴 ≤ 𝑤)) | |
4 | xrltle 12146 | . 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵)) | |
5 | 1, 2, 3, 4 | ixxssixx 12353 | 1 ⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 ∈ wcel 2127 ⊆ wss 3703 class class class wbr 4792 (class class class)co 6801 ℝ*cxr 10236 < clt 10237 ≤ cle 10238 [,)cico 12341 [,]cicc 12342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-pre-lttri 10173 ax-pre-lttrn 10174 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-op 4316 df-uni 4577 df-br 4793 df-opab 4853 df-mpt 4870 df-id 5162 df-po 5175 df-so 5176 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-er 7899 df-en 8110 df-dom 8111 df-sdom 8112 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-ico 12345 df-icc 12346 |
This theorem is referenced by: iccpnfcnv 22915 itg2mulclem 23683 itg2mulc 23684 itg2monolem1 23687 itg2monolem2 23688 itg2monolem3 23689 itg2mono 23690 itg2i1fseqle 23691 itg2i1fseq3 23694 itg2addlem 23695 itg2gt0 23697 itg2cnlem2 23699 psercnlem2 24348 eliccelico 29819 xrge0slmod 30124 xrge0iifcnv 30259 lmlimxrge0 30274 lmdvglim 30280 esumfsupre 30413 esumpfinvallem 30416 esumpfinval 30417 esumpfinvalf 30418 esumpcvgval 30420 esumpmono 30421 esummulc1 30423 sitmcl 30693 itg2addnc 33746 itg2gt0cn 33747 ftc1anclem6 33772 ftc1anclem8 33774 icoiccdif 40222 limciccioolb 40325 ltmod 40342 fourierdlem63 40858 fge0icoicc 41054 sge0tsms 41069 sge0iunmptlemre 41104 sge0isum 41116 sge0xaddlem1 41122 sge0xaddlem2 41123 sge0pnffsumgt 41131 sge0gtfsumgt 41132 sge0seq 41135 ovnsupge0 41246 ovnlecvr 41247 ovnsubaddlem1 41259 sge0hsphoire 41278 hoidmv1lelem3 41282 hoidmv1le 41283 hoidmvlelem1 41284 hoidmvlelem2 41285 hoidmvlelem3 41286 hoidmvlelem4 41287 hoidmvlelem5 41288 hoidmvle 41289 ovnhoilem1 41290 ovnlecvr2 41299 hspmbllem2 41316 |
Copyright terms: Public domain | W3C validator |