| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-icc | Structured version Visualization version GIF version | ||
| Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
| Ref | Expression |
|---|---|
| df-icc | ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cicc 13390 | . 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 | 7, 10, 8 | wbr 5143 | . . . . 5 wff 𝑧 ≤ 𝑦 |
| 12 | 9, 11 | wa 395 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) |
| 13 | 12, 6, 4 | crab 3436 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} |
| 14 | 2, 3, 4, 4, 13 | cmpo 7433 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| 15 | 1, 14 | wceq 1540 | 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: iccval 13426 elicc1 13431 iccss 13455 iccssioo 13456 iccss2 13458 iccssico 13459 iccssxr 13470 ioossicc 13473 icossicc 13476 iocssicc 13477 iccf 13488 ioounsn 13517 snunioo 13518 snunico 13519 snunioc 13520 ioodisj 13522 leordtval2 23220 iccordt 23222 lecldbas 23227 ioombl 25600 itgspliticc 25872 psercnlem2 26468 tanord1 26579 cvmliftlem10 35299 ftc1anclem7 37706 ftc1anclem8 37707 ftc1anc 37708 snunioo1 45525 iccin 48794 iccdisj2 48795 |
| Copyright terms: Public domain | W3C validator |