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 12047 | . 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 | cle 9954 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 4583 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 383 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 2900 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpt2 6551 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1475 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 12083 elioc1 12088 iocssxr 12128 iocssicc 12132 iocssioo 12134 snunioc 12171 leordtval2 20826 iocpnfordt 20829 lecldbas 20833 pnfnei 20834 iocmnfcld 22382 xrtgioo 22417 ismbf3d 23227 dvloglem 24194 asindmre 32665 dvasin 32666 ioounsn 36814 ioossioc 38560 snunioo2 38578 eliocre 38581 lbioc 38586 |
Copyright terms: Public domain | W3C validator |