Description: A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | iccid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc1 | |
|
2 | 1 | anidms | |
3 | xrlenlt | |
|
4 | xrlenlt | |
|
5 | 4 | ancoms | |
6 | xrlttri3 | |
|
7 | 6 | biimprd | |
8 | 7 | ancoms | |
9 | 8 | expcomd | |
10 | 5 9 | sylbid | |
11 | 10 | com23 | |
12 | 3 11 | sylbid | |
13 | 12 | ex | |
14 | 13 | 3impd | |
15 | eleq1a | |
|
16 | xrleid | |
|
17 | breq2 | |
|
18 | 16 17 | syl5ibrcom | |
19 | breq1 | |
|
20 | 16 19 | syl5ibrcom | |
21 | 15 18 20 | 3jcad | |
22 | 14 21 | impbid | |
23 | velsn | |
|
24 | 22 23 | bitr4di | |
25 | 2 24 | bitrd | |
26 | 25 | eqrdv | |