| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-ioc | Structured version Visualization version GIF version | ||
| Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
| Ref | Expression |
|---|---|
| df-ioc | ⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cioc 13388 | . 2 class (,] | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | vy | . . 3 setvar 𝑦 | |
| 4 | cxr 11294 | . . 3 class ℝ* | |
| 5 | 2 | cv 1539 | . . . . . 6 class 𝑥 |
| 6 | vz | . . . . . . 7 setvar 𝑧 | |
| 7 | 6 | cv 1539 | . . . . . 6 class 𝑧 |
| 8 | clt 11295 | . . . . . 6 class < | |
| 9 | 5, 7, 8 | wbr 5143 | . . . . 5 wff 𝑥 < 𝑧 |
| 10 | 3 | cv 1539 | . . . . . 6 class 𝑦 |
| 11 | cle 11296 | . . . . . 6 class ≤ | |
| 12 | 7, 10, 11 | wbr 5143 | . . . . 5 wff 𝑧 ≤ 𝑦 |
| 13 | 9, 12 | wa 395 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
| 14 | 13, 6, 4 | crab 3436 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
| 15 | 2, 3, 4, 4, 14 | cmpo 7433 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| 16 | 1, 15 | wceq 1540 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: iocval 13424 elioc1 13429 iocssxr 13471 iocssicc 13477 iocssioo 13479 ioounsn 13517 snunioc 13520 leordtval2 23220 iocpnfordt 23223 lecldbas 23227 pnfnei 23228 iocmnfcld 24789 xrtgioo 24828 ismbf3d 25689 dvloglem 26690 asindmre 37710 dvasin 37711 iocioodisjd 42355 ioossioc 45505 eliocre 45522 lbioc 45526 |
| Copyright terms: Public domain | W3C validator |