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 12728 | . 2 class (,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 10663 | . . 3 class ℝ* | |
5 | 2 | cv 1527 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1527 | . . . . . 6 class 𝑧 |
8 | clt 10664 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5058 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1527 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 5058 | . . . . 5 wff 𝑧 < 𝑦 |
12 | 9, 11 | wa 396 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦) |
13 | 12, 6, 4 | crab 3142 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpo 7147 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | 1, 14 | wceq 1528 | 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iooex 12751 iooval 12752 ndmioo 12755 elioo3g 12757 iooin 12762 iooss1 12763 iooss2 12764 elioo1 12768 iccssioo 12795 ioossicc 12812 ioossico 12816 iocssioo 12817 icossioo 12818 ioossioo 12819 ioof 12825 ioounsn 12853 snunioo 12854 ioodisj 12858 ioojoin 12859 ioopnfsup 13222 leordtval 21751 icopnfcld 23305 iocmnfcld 23306 bndth 23491 ioombl 24095 ioorf 24103 ioorinv2 24105 ismbf3d 24184 dvfsumrlimge0 24556 dvfsumrlim2 24558 tanord1 25048 dvloglem 25158 rlimcnp 25471 rlimcnp2 25472 dchrisum0lem2a 26021 pnt 26118 joiniooico 30424 tpr2rico 31055 asindmre 34859 dvasin 34860 ioossioc 41646 snunioo1 41668 ioossioobi 41673 |
Copyright terms: Public domain | W3C validator |