Description: A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl ). (Contributed by Paul Chapman, 21-Jan-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | iccsupr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccssre | |
|
2 | sstr | |
|
3 | 2 | ancoms | |
4 | 1 3 | sylan | |
5 | 4 | 3adant3 | |
6 | ne0i | |
|
7 | 6 | 3ad2ant3 | |
8 | simplr | |
|
9 | ssel | |
|
10 | elicc2 | |
|
11 | 10 | biimpd | |
12 | 9 11 | sylan9r | |
13 | 12 | imp | |
14 | 13 | simp3d | |
15 | 14 | ralrimiva | |
16 | brralrspcev | |
|
17 | 8 15 16 | syl2anc | |
18 | 17 | 3adant3 | |
19 | 5 7 18 | 3jca | |