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 12741 | . 2 class [,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10674 | . . 3 class ℝ* | |
5 | 2 | cv 1536 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1536 | . . . . . 6 class 𝑧 |
8 | cle 10676 | . . . . . 6 class ≤ | |
9 | 5, 7, 8 | wbr 5066 | . . . . 5 wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1536 | . . . . . 6 class 𝑦 |
11 | clt 10675 | . . . . . 6 class < | |
12 | 7, 10, 11 | wbr 5066 | . . . . 5 wff 𝑧 < 𝑦 |
13 | 9, 12 | wa 398 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
14 | 13, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7158 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 1, 15 | wceq 1537 | 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: icoval 12777 elico1 12782 elicore 12790 icossico 12807 iccssico 12809 iccssico2 12811 icossxr 12822 icossicc 12825 ioossico 12827 icossioo 12829 icoun 12862 snunioo 12865 snunico 12866 ioojoin 12870 icopnfsup 13234 limsupgord 14829 leordtval2 21820 icomnfordt 21824 lecldbas 21827 mnfnei 21829 icopnfcld 23376 xrtgioo 23414 ioombl 24166 dvfsumrlimge0 24627 dvfsumrlim2 24629 psercnlem2 25012 tanord1 25121 rlimcnp 25543 rlimcnp2 25544 dchrisum0lem2a 26093 pntleml 26187 pnt 26190 joiniooico 30497 icorempo 34635 icoreresf 34636 isbasisrelowl 34642 icoreelrn 34645 relowlpssretop 34648 asindmre 34992 icof 41502 snunioo1 41808 elicores 41829 dmico 41861 liminfgord 42055 volicorescl 42855 |
Copyright terms: Public domain | W3C validator |