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 12730 | . 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 | clt 10664 | . . . . . 6 class < | |
12 | 7, 10, 11 | wbr 5058 | . . . . 5 wff 𝑧 < 𝑦 |
13 | 9, 12 | wa 396 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
14 | 13, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7147 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 1, 15 | wceq 1528 | 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: icoval 12766 elico1 12771 elicore 12779 icossico 12796 iccssico 12798 iccssico2 12800 icossxr 12811 icossicc 12814 ioossico 12816 icossioo 12818 icoun 12851 snunioo 12854 snunico 12855 ioojoin 12859 icopnfsup 13223 limsupgord 14819 leordtval2 21750 icomnfordt 21754 lecldbas 21757 mnfnei 21759 icopnfcld 23305 xrtgioo 23343 ioombl 24095 dvfsumrlimge0 24556 dvfsumrlim2 24558 psercnlem2 24941 tanord1 25048 rlimcnp 25471 rlimcnp2 25472 dchrisum0lem2a 26021 pntleml 26115 pnt 26118 joiniooico 30424 icorempo 34515 icoreresf 34516 isbasisrelowl 34522 icoreelrn 34525 relowlpssretop 34528 asindmre 34859 icof 41362 snunioo1 41668 elicores 41689 dmico 41721 liminfgord 41915 volicorescl 42716 |
Copyright terms: Public domain | W3C validator |