![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ioossioo | Structured version Visualization version GIF version |
Description: Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
Ref | Expression |
---|---|
ioossioo | ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo 12558 | . 2 ⊢ (,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)}) | |
2 | xrlelttr 12366 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴 ≤ 𝐶 ∧ 𝐶 < 𝑤) → 𝐴 < 𝑤)) | |
3 | xrltletr 12367 | . 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝑤 < 𝐷 ∧ 𝐷 ≤ 𝐵) → 𝑤 < 𝐵)) | |
4 | 1, 1, 2, 3 | ixxss12 12574 | 1 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 ⊆ wss 3830 class class class wbr 4929 (class class class)co 6976 ℝ*cxr 10473 < clt 10474 ≤ cle 10475 (,)cioo 12554 |
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 2751 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-pre-lttri 10409 ax-pre-lttrn 10410 |
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 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-id 5312 df-po 5326 df-so 5327 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-ov 6979 df-oprab 6980 df-mpo 6981 df-1st 7501 df-2nd 7502 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-ioo 12558 |
This theorem is referenced by: difioo 30257 tpr2rico 30796 signsply0 31464 ftc1cnnclem 34403 ftc1anclem7 34411 ftc1anclem8 34412 ftc1anc 34413 ftc2nc 34414 ioossioobi 41222 dvbdfbdioolem1 41641 fourierdlem20 41841 fourierdlem72 41892 fourierdlem79 41899 fourierdlem103 41923 fourierdlem104 41924 ioorrnopnxrlem 42020 |
Copyright terms: Public domain | W3C validator |