![]() |
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 13309 | . 2 class [,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 11229 | . . 3 class ℝ* | |
5 | 2 | cv 1540 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1540 | . . . . . 6 class 𝑧 |
8 | cle 11231 | . . . . . 6 class ≤ | |
9 | 5, 7, 8 | wbr 5141 | . . . . 5 wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1540 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 5141 | . . . . 5 wff 𝑧 ≤ 𝑦 |
12 | 9, 11 | wa 396 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) |
13 | 12, 6, 4 | crab 3431 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpo 7395 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
15 | 1, 14 | wceq 1541 | 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iccval 13345 elicc1 13350 iccss 13374 iccssioo 13375 iccss2 13377 iccssico 13378 iccssxr 13389 ioossicc 13392 icossicc 13395 iocssicc 13396 iccf 13407 ioounsn 13436 snunioo 13437 snunico 13438 snunioc 13439 ioodisj 13441 leordtval2 22645 iccordt 22647 lecldbas 22652 ioombl 25011 itgspliticc 25283 psercnlem2 25865 tanord1 25975 cvmliftlem10 34116 ftc1anclem7 36371 ftc1anclem8 36372 ftc1anc 36373 snunioo1 43998 iccin 47177 iccdisj2 47178 |
Copyright terms: Public domain | W3C validator |