![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-icc | 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 10875 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cxr 9075 |
. . 3
![]() ![]() | |
5 | 2 | cv 1648 |
. . . . . 6
![]() ![]() |
6 | vz |
. . . . . . 7
![]() ![]() | |
7 | 6 | cv 1648 |
. . . . . 6
![]() ![]() |
8 | cle 9077 |
. . . . . 6
![]() ![]() | |
9 | 5, 7, 8 | wbr 4172 |
. . . . 5
![]() ![]() ![]() ![]() |
10 | 3 | cv 1648 |
. . . . . 6
![]() ![]() |
11 | 7, 10, 8 | wbr 4172 |
. . . . 5
![]() ![]() ![]() ![]() |
12 | 9, 11 | wa 359 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12, 6, 4 | crab 2670 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 2, 3, 4, 4, 13 | cmpt2 6042 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 14 | wceq 1649 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: iccval 10911 elicc1 10916 iccss 10934 iccssioo 10935 iccss2 10937 iccssico 10938 iccssxr 10949 ioossicc 10952 iccf 10959 snunioo 10979 snunico 10980 ioodisj 10982 leordtval2 17230 iccordt 17232 lecldbas 17237 ioombl 19412 itg2mulclem 19591 itg2mulc 19592 itgspliticc 19681 psercnlem2 20293 tanord1 20392 icossicc 24082 iocssicc 24083 snunioc 24090 cvmliftlem10 24934 |
Copyright terms: Public domain | W3C validator |