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 12816 | . 2 class [,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10745 | . . 3 class ℝ* | |
5 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1541 | . . . . . 6 class 𝑧 |
8 | cle 10747 | . . . . . 6 class ≤ | |
9 | 5, 7, 8 | wbr 5027 | . . . . 5 wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1541 | . . . . . 6 class 𝑦 |
11 | clt 10746 | . . . . . 6 class < | |
12 | 7, 10, 11 | wbr 5027 | . . . . 5 wff 𝑧 < 𝑦 |
13 | 9, 12 | wa 399 | . . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
14 | 13, 6, 4 | crab 3057 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 7166 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 1, 15 | wceq 1542 | 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: icoval 12852 elico1 12857 elicore 12866 icossico 12884 iccssico 12886 iccssico2 12888 icossxr 12899 icossicc 12903 ioossico 12905 icossioo 12907 icoun 12942 snunioo 12945 snunico 12946 ioojoin 12950 icopnfsup 13317 limsupgord 14912 leordtval2 21956 icomnfordt 21960 lecldbas 21963 mnfnei 21965 icopnfcld 23513 xrtgioo 23551 ioombl 24310 dvfsumrlimge0 24774 dvfsumrlim2 24776 psercnlem2 25163 tanord1 25273 rlimcnp 25695 rlimcnp2 25696 dchrisum0lem2a 26245 pntleml 26339 pnt 26342 joiniooico 30662 icorempo 35134 icoreresf 35135 isbasisrelowl 35141 icoreelrn 35144 relowlpssretop 35147 asindmre 35472 icof 42281 snunioo1 42574 elicores 42595 dmico 42627 liminfgord 42821 volicorescl 43617 iccdisj2 45698 |
Copyright terms: Public domain | W3C validator |