| 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 13387 | . 2 class (,) | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | vy | . . 3 setvar 𝑦 | |
| 4 | cxr 11294 | . . 3 class ℝ* | |
| 5 | 2 | cv 1539 | . . . . . 6 class 𝑥 |
| 6 | vz | . . . . . . 7 setvar 𝑧 | |
| 7 | 6 | cv 1539 | . . . . . 6 class 𝑧 |
| 8 | clt 11295 | . . . . . 6 class < | |
| 9 | 5, 7, 8 | wbr 5143 | . . . . 5 wff 𝑥 < 𝑧 |
| 10 | 3 | cv 1539 | . . . . . 6 class 𝑦 |
| 11 | 7, 10, 8 | wbr 5143 | . . . . 5 wff 𝑧 < 𝑦 |
| 12 | 9, 11 | wa 395 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦) |
| 13 | 12, 6, 4 | crab 3436 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} |
| 14 | 2, 3, 4, 4, 13 | cmpo 7433 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| 15 | 1, 14 | wceq 1540 | 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: iooex 13410 iooval 13411 ndmioo 13414 elioo3g 13416 iooin 13421 iooss1 13422 iooss2 13423 elioo1 13427 iccssioo 13456 ioossicc 13473 ioossico 13478 iocssioo 13479 icossioo 13480 ioossioo 13481 ioof 13487 ioounsn 13517 snunioo 13518 ioodisj 13522 ioojoin 13523 ioopnfsup 13904 leordtval 23221 icopnfcld 24788 iocmnfcld 24789 bndth 24990 ioombl 25600 ioorf 25608 ioorinv2 25610 ismbf3d 25689 dvfsumrlimge0 26071 dvfsumrlim2 26073 tanord1 26579 dvloglem 26690 rlimcnp 27008 rlimcnp2 27009 dchrisum0lem2a 27561 pnt 27658 joiniooico 32776 tpr2rico 33911 asindmre 37710 dvasin 37711 iocioodisjd 42355 ioossioc 45505 snunioo1 45525 ioossioobi 45530 |
| Copyright terms: Public domain | W3C validator |