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 12049 | . 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 | 7, 10, 8 | wbr 4583 | . . . . 5 wff 𝑧 ≤ 𝑦 |
12 | 9, 11 | wa 383 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) |
13 | 12, 6, 4 | crab 2900 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpt2 6551 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
15 | 1, 14 | wceq 1475 | 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iccval 12085 elicc1 12090 iccss 12112 iccssioo 12113 iccss2 12115 iccssico 12116 iccssxr 12127 ioossicc 12130 icossicc 12131 iocssicc 12132 iccf 12143 snunioo 12169 snunico 12170 snunioc 12171 ioodisj 12173 leordtval2 20826 iccordt 20828 lecldbas 20833 ioombl 23140 itgspliticc 23409 psercnlem2 23982 tanord1 24087 cvmliftlem10 30530 ftc1anclem7 32661 ftc1anclem8 32662 ftc1anc 32663 ioounsn 36814 snunioo2 38578 snunioo1 38585 |
Copyright terms: Public domain | W3C validator |