![]() |
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 13379 | . 2 class (,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 11297 | . . 3 class ℝ* | |
5 | 2 | cv 1533 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1533 | . . . . . 6 class 𝑧 |
8 | clt 11298 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5153 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1533 | . . . . . 6 class 𝑦 |
11 | cle 11299 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 5153 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 394 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 3419 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7426 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1534 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 13415 elioc1 13420 iocssxr 13462 iocssicc 13468 iocssioo 13470 ioounsn 13508 snunioc 13511 leordtval2 23207 iocpnfordt 23210 lecldbas 23214 pnfnei 23215 iocmnfcld 24776 xrtgioo 24813 ismbf3d 25674 dvloglem 26675 asindmre 37404 dvasin 37405 ioossioc 45110 eliocre 45127 lbioc 45131 |
Copyright terms: Public domain | W3C validator |