Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ioo | Structured version Visualization version GIF version |
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
df-ioo | ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cioo 12739 | . 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 | clt 10675 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5066 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1536 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 5066 | . . . . 5 wff 𝑧 < 𝑦 |
12 | 9, 11 | wa 398 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦) |
13 | 12, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpo 7158 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | 1, 14 | wceq 1537 | 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iooex 12762 iooval 12763 ndmioo 12766 elioo3g 12768 iooin 12773 iooss1 12774 iooss2 12775 elioo1 12779 iccssioo 12806 ioossicc 12823 ioossico 12827 iocssioo 12828 icossioo 12829 ioossioo 12830 ioof 12836 ioounsn 12864 snunioo 12865 ioodisj 12869 ioojoin 12870 ioopnfsup 13233 leordtval 21821 icopnfcld 23376 iocmnfcld 23377 bndth 23562 ioombl 24166 ioorf 24174 ioorinv2 24176 ismbf3d 24255 dvfsumrlimge0 24627 dvfsumrlim2 24629 tanord1 25121 dvloglem 25231 rlimcnp 25543 rlimcnp2 25544 dchrisum0lem2a 26093 pnt 26190 joiniooico 30497 tpr2rico 31155 asindmre 34992 dvasin 34993 ioossioc 41815 snunioo1 41837 ioossioobi 41842 |
Copyright terms: Public domain | W3C validator |