![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-ioc | Structured version Visualization version Unicode version |
Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
df-ioc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cioc 11626 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cxr 9661 |
. . 3
![]() ![]() | |
5 | 2 | cv 1447 |
. . . . . 6
![]() ![]() |
6 | vz |
. . . . . . 7
![]() ![]() | |
7 | 6 | cv 1447 |
. . . . . 6
![]() ![]() |
8 | clt 9662 |
. . . . . 6
![]() ![]() | |
9 | 5, 7, 8 | wbr 4374 |
. . . . 5
![]() ![]() ![]() ![]() |
10 | 3 | cv 1447 |
. . . . . 6
![]() ![]() |
11 | cle 9663 |
. . . . . 6
![]() ![]() | |
12 | 7, 10, 11 | wbr 4374 |
. . . . 5
![]() ![]() ![]() ![]() |
13 | 9, 12 | wa 375 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 6, 4 | crab 2741 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 2, 3, 4, 4, 14 | cmpt2 6278 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 1, 15 | wceq 1448 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: iocval 11663 elioc1 11668 iocssxr 11708 iocssicc 11712 iocssioo 11714 snunioc 11751 leordtval2 20239 iocpnfordt 20242 lecldbas 20246 pnfnei 20247 iocmnfcld 21800 xrtgioo 21835 ismbf3d 22622 dvloglem 23605 asindmre 32029 dvasin 32030 ioounsn 36096 ioossioc 37629 snunioo2 37647 eliocre 37650 lbioc 37655 |
Copyright terms: Public domain | W3C validator |