![]() |
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 12727 | . 2 class (,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10663 | . . 3 class ℝ* | |
5 | 2 | cv 1537 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1537 | . . . . . 6 class 𝑧 |
8 | clt 10664 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5030 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1537 | . . . . . 6 class 𝑦 |
11 | cle 10665 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 5030 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 399 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 3110 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7137 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1538 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 12763 elioc1 12768 iocssxr 12809 iocssicc 12815 iocssioo 12817 ioounsn 12855 snunioc 12858 leordtval2 21817 iocpnfordt 21820 lecldbas 21824 pnfnei 21825 iocmnfcld 23374 xrtgioo 23411 ismbf3d 24258 dvloglem 25239 asindmre 35140 dvasin 35141 ioossioc 42129 eliocre 42146 lbioc 42150 |
Copyright terms: Public domain | W3C validator |