![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iooss1 | Structured version Visualization version GIF version |
Description: Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
Ref | Expression |
---|---|
iooss1 | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo 12561 | . 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | |
2 | xrlelttr 12369 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝑤) → 𝐴 < 𝑤)) | |
3 | 1, 1, 2 | ixxss1 12575 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 ⊆ wss 3831 class class class wbr 4930 (class class class)co 6978 ℝ*cxr 10475 < clt 10476 ≤ cle 10477 (,)cioo 12557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-pre-lttri 10411 ax-pre-lttrn 10412 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-po 5327 df-so 5328 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-ov 6981 df-oprab 6982 df-mpo 6983 df-1st 7503 df-2nd 7504 df-er 8091 df-en 8309 df-dom 8310 df-sdom 8311 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-ioo 12561 |
This theorem is referenced by: ioodisj 12687 tgqioo 23114 ioorcl2 23879 itg2gt0 24067 itgsplitioo 24144 ditgcl 24162 ditgswap 24163 ditgsplitlem 24164 dvferm1lem 24287 dvferm 24291 dvlip 24296 dvgt0lem1 24305 dvivthlem1 24311 lhop1lem 24316 lhop2 24318 dvcvx 24323 dvfsumle 24324 dvfsumge 24325 dvfsumabs 24326 ftc1lem1 24338 ftc1a 24340 ftc1lem4 24342 ftc2ditglem 24348 tanregt0 24827 basellem4 25366 pntlemp 25891 radcnvrat 40062 limcresiooub 41355 fourierdlem46 41869 fourierdlem48 41871 fourierdlem49 41872 fourierdlem74 41897 fourierdlem104 41927 fourierdlem113 41936 fouriersw 41948 |
Copyright terms: Public domain | W3C validator |