Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ico | Structured version Visualization version 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 12048 | . 2 class [,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 9952 | . . 3 class ℝ* | |
5 | 2 | cv 1474 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1474 | . . . . . 6 class 𝑧 |
8 | cle 9954 | . . . . . 6 class ≤ | |
9 | 5, 7, 8 | wbr 4583 | . . . . 5 wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1474 | . . . . . 6 class 𝑦 |
11 | clt 9953 | . . . . . 6 class < | |
12 | 7, 10, 11 | wbr 4583 | . . . . 5 wff 𝑧 < 𝑦 |
13 | 9, 12 | wa 383 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
14 | 13, 6, 4 | crab 2900 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpt2 6551 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 1, 15 | wceq 1475 | 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: icoval 12084 elico1 12089 elicore 12097 icossico 12114 iccssico 12116 iccssico2 12118 icossxr 12129 icossicc 12131 ioossico 12133 icossioo 12135 icoun 12167 snunioo 12169 snunico 12170 ioojoin 12174 icopnfsup 12526 limsupgord 14051 leordtval2 20826 icomnfordt 20830 lecldbas 20833 mnfnei 20835 icopnfcld 22381 xrtgioo 22417 ioombl 23140 dvfsumrlimge0 23597 dvfsumrlim2 23599 psercnlem2 23982 tanord1 24087 rlimcnp 24492 rlimcnp2 24493 dchrisum0lem2a 25006 pntleml 25100 pnt 25103 joiniooico 28926 icorempt2 32375 icoreresf 32376 isbasisrelowl 32382 icoreelrn 32385 relowlpssretop 32388 asindmre 32665 icof 38406 snunioo1 38585 elicores 38607 volicorescl 39443 |
Copyright terms: Public domain | W3C validator |