![]() |
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 12558 | . 2 ⊢ [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 < 𝑏)}) | |
2 | df-icc 12559 | . 2 ⊢ [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 ≤ 𝑥 ∧ 𝑥 ≤ 𝑏)}) | |
3 | idd 24 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 ≤ 𝑤 → 𝐴 ≤ 𝑤)) | |
4 | xrltle 12357 | . 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵)) | |
5 | 1, 2, 3, 4 | ixxssixx 12566 | 1 ⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 ∈ wcel 2051 ⊆ wss 3822 class class class wbr 4925 (class class class)co 6974 ℝ*cxr 10471 < clt 10472 ≤ cle 10473 [,)cico 12554 [,]cicc 12555 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-cnex 10389 ax-resscn 10390 ax-pre-lttri 10407 ax-pre-lttrn 10408 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-nel 3067 df-ral 3086 df-rex 3087 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-po 5322 df-so 5323 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-ov 6977 df-oprab 6978 df-mpo 6979 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-pnf 10474 df-mnf 10475 df-xr 10476 df-ltxr 10477 df-le 10478 df-ico 12558 df-icc 12559 |
This theorem is referenced by: iccpnfcnv 23266 itg2mulclem 24065 itg2mulc 24066 itg2monolem1 24069 itg2monolem2 24070 itg2monolem3 24071 itg2mono 24072 itg2i1fseq3 24076 itg2addlem 24077 itg2gt0 24079 itg2cnlem2 24081 psercnlem2 24730 eliccelico 30276 xrge0slmod 30628 xrge0iifcnv 30852 lmlimxrge0 30867 lmdvglim 30873 esumfsupre 31006 esumpfinvallem 31009 esumpfinval 31010 esumpfinvalf 31011 esumpcvgval 31013 esumpmono 31014 esummulc1 31016 sitmcl 31286 itg2addnc 34424 itg2gt0cn 34425 ftc1anclem6 34450 ftc1anclem8 34452 icoiccdif 41265 limciccioolb 41367 ltmod 41384 fourierdlem63 41919 fge0icoicc 42112 sge0tsms 42127 sge0iunmptlemre 42162 sge0isum 42174 sge0xaddlem1 42180 sge0xaddlem2 42181 sge0pnffsumgt 42189 sge0gtfsumgt 42190 sge0seq 42193 ovnsupge0 42304 ovnlecvr 42305 ovnsubaddlem1 42317 sge0hsphoire 42336 hoidmv1lelem3 42340 hoidmv1le 42341 hoidmvlelem1 42342 hoidmvlelem2 42343 hoidmvlelem3 42344 hoidmvlelem4 42345 hoidmvlelem5 42346 hoidmvle 42347 ovnhoilem1 42348 ovnlecvr2 42357 hspmbllem2 42374 |
Copyright terms: Public domain | W3C validator |