![]() |
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 13319 | . 2 class (,) | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cxr 11242 | . . 3 class ℝ* | |
5 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1541 | . . . . . 6 class 𝑧 |
8 | clt 11243 | . . . . . 6 class < | |
9 | 5, 7, 8 | wbr 5146 | . . . . 5 wff 𝑥 < 𝑧 |
10 | 3 | cv 1541 | . . . . . 6 class 𝑦 |
11 | 7, 10, 8 | wbr 5146 | . . . . 5 wff 𝑧 < 𝑦 |
12 | 9, 11 | wa 397 | . . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦) |
13 | 12, 6, 4 | crab 3433 | . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)} |
14 | 2, 3, 4, 4, 13 | cmpo 7405 | . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | 1, 14 | wceq 1542 | 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: iooex 13342 iooval 13343 ndmioo 13346 elioo3g 13348 iooin 13353 iooss1 13354 iooss2 13355 elioo1 13359 iccssioo 13388 ioossicc 13405 ioossico 13410 iocssioo 13411 icossioo 13412 ioossioo 13413 ioof 13419 ioounsn 13449 snunioo 13450 ioodisj 13454 ioojoin 13455 ioopnfsup 13824 leordtval 22698 icopnfcld 24265 iocmnfcld 24266 bndth 24455 ioombl 25063 ioorf 25071 ioorinv2 25073 ismbf3d 25152 dvfsumrlimge0 25528 dvfsumrlim2 25530 tanord1 26027 dvloglem 26137 rlimcnp 26449 rlimcnp2 26450 dchrisum0lem2a 26999 pnt 27096 joiniooico 31962 tpr2rico 32829 asindmre 36508 dvasin 36509 ioossioc 44139 snunioo1 44159 ioossioobi 44164 |
Copyright terms: Public domain | W3C validator |