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 12731 | . 2 class [,] | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10663 | . . 3 class ℝ* | |
5 | 2 | cv 1527 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1527 | . . . . . 6 class 𝑧 |
8 | cle 10665 | . . . . . 6 class ≤ | |
9 | 5, 7, 8 | wbr 5058 | . . . . 5 wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1527 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 5058 | . . . . 5 wff 𝑧 ≤ 𝑦 |
12 | 9, 11 | wa 396 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) |
13 | 12, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpo 7147 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
15 | 1, 14 | wceq 1528 | 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iccval 12767 elicc1 12772 iccss 12794 iccssioo 12795 iccss2 12797 iccssico 12798 iccssxr 12809 ioossicc 12812 icossicc 12814 iocssicc 12815 iccf 12826 ioounsn 12853 snunioo 12854 snunico 12855 snunioc 12856 ioodisj 12858 leordtval2 21750 iccordt 21752 lecldbas 21757 ioombl 24095 itgspliticc 24366 psercnlem2 24941 tanord1 25048 cvmliftlem10 32439 ftc1anclem7 34855 ftc1anclem8 34856 ftc1anc 34857 snunioo1 41668 |
Copyright terms: Public domain | W3C validator |