Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ioo | Structured version Visualization version GIF version |
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
df-ioo | ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cioo 12046 | . 2 class (,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 9952 | . . 3 class ℝ* | |
5 | 2 | cv 1474 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1474 | . . . . . 6 class 𝑧 |
8 | clt 9953 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 4583 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1474 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 4583 | . . . . 5 wff 𝑧 < 𝑦 |
12 | 9, 11 | wa 383 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦) |
13 | 12, 6, 4 | crab 2900 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpt2 6551 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | 1, 14 | wceq 1475 | 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iooex 12069 iooval 12070 ndmioo 12073 elioo3g 12075 iooin 12080 iooss1 12081 iooss2 12082 elioo1 12086 iccssioo 12113 ioossicc 12130 ioossico 12133 iocssioo 12134 icossioo 12135 ioossioo 12136 ioof 12142 snunioo 12169 ioodisj 12173 ioojoin 12174 ioopnfsup 12525 leordtval 20827 icopnfcld 22381 iocmnfcld 22382 bndth 22565 ioombl 23140 ioorf 23147 ioorinv2 23149 ismbf3d 23227 dvfsumrlimge0 23597 dvfsumrlim2 23599 tanord1 24087 dvloglem 24194 rlimcnp 24492 rlimcnp2 24493 dchrisum0lem2a 25006 pnt 25103 joiniooico 28926 tpr2rico 29286 asindmre 32665 dvasin 32666 ioounsn 36814 ioossioc 38560 snunioo2 38578 snunioo1 38585 ioossioobi 38590 |
Copyright terms: Public domain | W3C validator |