![]() |
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 13322 | . 2 class (,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 11244 | . . 3 class ℝ* | |
5 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1541 | . . . . . 6 class 𝑧 |
8 | clt 11245 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5148 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1541 | . . . . . 6 class 𝑦 |
11 | cle 11246 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 5148 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 397 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 3433 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7408 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1542 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 13358 elioc1 13363 iocssxr 13405 iocssicc 13411 iocssioo 13413 ioounsn 13451 snunioc 13454 leordtval2 22708 iocpnfordt 22711 lecldbas 22715 pnfnei 22716 iocmnfcld 24277 xrtgioo 24314 ismbf3d 25163 dvloglem 26148 asindmre 36560 dvasin 36561 ioossioc 44192 eliocre 44209 lbioc 44213 |
Copyright terms: Public domain | W3C validator |