![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-icc | Structured version Visualization version Unicode version |
Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
df-icc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cicc 11638 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cxr 9674 |
. . 3
![]() ![]() | |
5 | 2 | cv 1443 |
. . . . . 6
![]() ![]() |
6 | vz |
. . . . . . 7
![]() ![]() | |
7 | 6 | cv 1443 |
. . . . . 6
![]() ![]() |
8 | cle 9676 |
. . . . . 6
![]() ![]() | |
9 | 5, 7, 8 | wbr 4402 |
. . . . 5
![]() ![]() ![]() ![]() |
10 | 3 | cv 1443 |
. . . . . 6
![]() ![]() |
11 | 7, 10, 8 | wbr 4402 |
. . . . 5
![]() ![]() ![]() ![]() |
12 | 9, 11 | wa 371 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12, 6, 4 | crab 2741 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 2, 3, 4, 4, 13 | cmpt2 6292 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 14 | wceq 1444 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: iccval 11675 elicc1 11680 iccss 11702 iccssioo 11703 iccss2 11705 iccssico 11706 iccssxr 11717 ioossicc 11720 icossicc 11721 iocssicc 11722 iccf 11733 snunioo 11758 snunico 11759 snunioc 11760 ioodisj 11762 leordtval2 20228 iccordt 20230 lecldbas 20235 ioombl 22518 itgspliticc 22794 psercnlem2 23379 tanord1 23486 cvmliftlem10 30017 ftc1anclem7 32023 ftc1anclem8 32024 ftc1anc 32025 ioounsn 36094 snunioo2 37606 snunioo1 37613 |
Copyright terms: Public domain | W3C validator |