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 12814 | . 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 | clt 10746 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5027 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1541 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 5027 | . . . . 5 wff 𝑧 < 𝑦 |
12 | 9, 11 | wa 399 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦) |
13 | 12, 6, 4 | crab 3057 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpo 7166 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | 1, 14 | wceq 1542 | 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iooex 12837 iooval 12838 ndmioo 12841 elioo3g 12843 iooin 12848 iooss1 12849 iooss2 12850 elioo1 12854 iccssioo 12883 ioossicc 12900 ioossico 12905 iocssioo 12906 icossioo 12907 ioossioo 12908 ioof 12914 ioounsn 12944 snunioo 12945 ioodisj 12949 ioojoin 12950 ioopnfsup 13316 leordtval 21957 icopnfcld 23513 iocmnfcld 23514 bndth 23703 ioombl 24310 ioorf 24318 ioorinv2 24320 ismbf3d 24399 dvfsumrlimge0 24774 dvfsumrlim2 24776 tanord1 25273 dvloglem 25383 rlimcnp 25695 rlimcnp2 25696 dchrisum0lem2a 26245 pnt 26342 joiniooico 30662 tpr2rico 31426 asindmre 35472 dvasin 35473 ioossioc 42554 snunioo1 42574 ioossioobi 42579 |
Copyright terms: Public domain | W3C validator |