![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iooss2 | 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, 3-Nov-2013.) |
Ref | Expression |
---|---|
iooss2 | ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo 13384 | . 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | |
2 | xrltletr 13192 | . 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝑤 < 𝐶)) | |
3 | 1, 1, 2 | ixxss2 13399 | 1 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2099 ⊆ wss 3947 class class class wbr 5155 (class class class)co 7426 ℝ*cxr 11299 < clt 11300 ≤ cle 11301 (,)cioo 13380 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5306 ax-nul 5313 ax-pow 5371 ax-pr 5435 ax-un 7748 ax-cnex 11216 ax-resscn 11217 ax-pre-lttri 11234 ax-pre-lttrn 11235 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4916 df-iun 5005 df-br 5156 df-opab 5218 df-mpt 5239 df-id 5582 df-po 5596 df-so 5597 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6508 df-fun 6558 df-fn 6559 df-f 6560 df-f1 6561 df-fo 6562 df-f1o 6563 df-fv 6564 df-ov 7429 df-oprab 7430 df-mpo 7431 df-1st 8005 df-2nd 8006 df-er 8736 df-en 8977 df-dom 8978 df-sdom 8979 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-ioo 13384 |
This theorem is referenced by: tgqioo 24810 ioorcl2 25595 itgsplitioo 25861 ditgcl 25881 ditgswap 25882 ditgsplitlem 25883 dvferm2lem 26012 dvferm 26014 dvlip 26020 dvgt0lem1 26029 dvivthlem1 26035 lhop1lem 26040 lhop1 26041 dvcvx 26047 dvfsumle 26048 dvfsumleOLD 26049 dvfsumge 26050 dvfsumabs 26051 ftc1lem1 26064 ftc1lem2 26065 ftc1a 26066 ftc1lem4 26068 ftc2 26073 ftc2ditglem 26074 itgsubstlem 26077 cos0pilt1 26562 ftc1anc 37404 ftc2nc 37405 limcresioolb 45282 fourierdlem46 45791 fourierdlem48 45793 fourierdlem49 45794 fourierdlem75 45820 fourierdlem103 45848 fourierdlem113 45858 fouriersw 45870 |
Copyright terms: Public domain | W3C validator |