![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ico | GIF version |
Description: Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
df-ico | ⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cico 9889 | . 2 class [,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 7990 | . . 3 class ℝ* | |
5 | 2 | cv 1352 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1352 | . . . . . 6 class 𝑧 |
8 | cle 7992 | . . . . . 6 class ≤ | |
9 | 5, 7, 8 | wbr 4003 | . . . . 5 wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1352 | . . . . . 6 class 𝑦 |
11 | clt 7991 | . . . . . 6 class < | |
12 | 7, 10, 11 | wbr 4003 | . . . . 5 wff 𝑧 < 𝑦 |
13 | 9, 12 | wa 104 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
14 | 13, 6, 4 | crab 2459 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 5876 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 1, 15 | wceq 1353 | 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff set class |
This definition is referenced by: icoval 9918 elico1 9922 icossico 9942 iccssico 9944 iccssico2 9946 icossxr 9957 icossicc 9959 ioossico 9961 icossioo 9963 elicore 10266 |
Copyright terms: Public domain | W3C validator |