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 12740 | . 2 class (,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10674 | . . 3 class ℝ* | |
5 | 2 | cv 1536 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1536 | . . . . . 6 class 𝑧 |
8 | clt 10675 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5066 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1536 | . . . . . 6 class 𝑦 |
11 | cle 10676 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 5066 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 398 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7158 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1537 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 12776 elioc1 12781 iocssxr 12821 iocssicc 12826 iocssioo 12828 ioounsn 12864 snunioc 12867 leordtval2 21820 iocpnfordt 21823 lecldbas 21827 pnfnei 21828 iocmnfcld 23377 xrtgioo 23414 ismbf3d 24255 dvloglem 25231 asindmre 34992 dvasin 34993 ioossioc 41815 eliocre 41834 lbioc 41838 |
Copyright terms: Public domain | W3C validator |