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 12815 | . 2 class (,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10745 | . . 3 class ℝ* | |
5 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1541 | . . . . . 6 class 𝑧 |
8 | clt 10746 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5027 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1541 | . . . . . 6 class 𝑦 |
11 | cle 10747 | . . . . . 6 class ≤ | |
12 | 7, 10, 11 | wbr 5027 | . . . . 5 wff 𝑧 ≤ 𝑦 |
13 | 9, 12 | wa 399 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦) |
14 | 13, 6, 4 | crab 3057 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7166 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
16 | 1, 15 | wceq 1542 | 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 12851 elioc1 12856 iocssxr 12898 iocssicc 12904 iocssioo 12906 ioounsn 12944 snunioc 12947 leordtval2 21956 iocpnfordt 21959 lecldbas 21963 pnfnei 21964 iocmnfcld 23514 xrtgioo 23551 ismbf3d 24399 dvloglem 25383 asindmre 35472 dvasin 35473 ioossioc 42554 eliocre 42571 lbioc 42575 |
Copyright terms: Public domain | W3C validator |