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 12729 | . 2 class (,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10663 | . . 3 class ℝ* | |
5 | 2 | cv 1527 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1527 | . . . . . 6 class 𝑧 |
8 | clt 10664 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5058 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1527 | . . . . . 6 class 𝑦 |
11 | cle 10665 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 5058 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 396 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7147 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1528 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 12765 elioc1 12770 iocssxr 12810 iocssicc 12815 iocssioo 12817 ioounsn 12853 snunioc 12856 leordtval2 21750 iocpnfordt 21753 lecldbas 21757 pnfnei 21758 iocmnfcld 23306 xrtgioo 23343 ismbf3d 24184 dvloglem 25158 asindmre 34859 dvasin 34860 ioossioc 41646 eliocre 41665 lbioc 41669 |
Copyright terms: Public domain | W3C validator |