Metamath Proof Explorer


Theorem iccsupr

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 ABSABCSSSxySyx

Proof

Step Hyp Ref Expression
1 iccssre ABAB
2 sstr SABABS
3 2 ancoms ABSABS
4 1 3 sylan ABSABS
5 4 3adant3 ABSABCSS
6 ne0i CSS
7 6 3ad2ant3 ABSABCSS
8 simplr ABSABB
9 ssel SABySyAB
10 elicc2 AByAByAyyB
11 10 biimpd AByAByAyyB
12 9 11 sylan9r ABSABySyAyyB
13 12 imp ABSABySyAyyB
14 13 simp3d ABSABySyB
15 14 ralrimiva ABSABySyB
16 brralrspcev BySyBxySyx
17 8 15 16 syl2anc ABSABxySyx
18 17 3adant3 ABSABCSxySyx
19 5 7 18 3jca ABSABCSSSxySyx