| 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 13389 | . 2 class [,) | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | vy | . . 3 setvar 𝑦 | |
| 4 | cxr 11294 | . . 3 class ℝ* | |
| 5 | 2 | cv 1539 | . . . . . 6 class 𝑥 |
| 6 | vz | . . . . . . 7 setvar 𝑧 | |
| 7 | 6 | cv 1539 | . . . . . 6 class 𝑧 |
| 8 | cle 11296 | . . . . . 6 class ≤ | |
| 9 | 5, 7, 8 | wbr 5143 | . . . . 5 wff 𝑥 ≤ 𝑧 |
| 10 | 3 | cv 1539 | . . . . . 6 class 𝑦 |
| 11 | clt 11295 | . . . . . 6 class < | |
| 12 | 7, 10, 11 | wbr 5143 | . . . . 5 wff 𝑧 < 𝑦 |
| 13 | 9, 12 | wa 395 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
| 14 | 13, 6, 4 | crab 3436 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
| 15 | 2, 3, 4, 4, 14 | cmpo 7433 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 16 | 1, 15 | wceq 1540 | 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: icoval 13425 elico1 13430 elicore 13439 icossico 13457 iccssico 13459 iccssico2 13461 icossxr 13472 icossicc 13476 ioossico 13478 icossioo 13480 icoun 13515 snunioo 13518 snunico 13519 ioojoin 13523 icopnfsup 13905 limsupgord 15508 leordtval2 23220 icomnfordt 23224 lecldbas 23227 mnfnei 23229 icopnfcld 24788 xrtgioo 24828 ioombl 25600 dvfsumrlimge0 26071 dvfsumrlim2 26073 psercnlem2 26468 tanord1 26579 rlimcnp 27008 rlimcnp2 27009 dchrisum0lem2a 27561 pntleml 27655 pnt 27658 joiniooico 32776 icorempo 37352 icoreresf 37353 isbasisrelowl 37359 icoreelrn 37362 relowlpssretop 37365 asindmre 37710 icof 45224 snunioo1 45525 elicores 45546 dmico 45578 liminfgord 45769 volicorescl 46568 iccdisj2 48795 |
| Copyright terms: Public domain | W3C validator |