Metamath Proof Explorer


Theorem xrsupssd

Description: Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017)

Ref Expression
Hypotheses xrsupssd.1
|- ( ph -> B C_ C )
xrsupssd.2
|- ( ph -> C C_ RR* )
Assertion xrsupssd
|- ( ph -> sup ( B , RR* , < ) <_ sup ( C , RR* , < ) )

Proof

Step Hyp Ref Expression
1 xrsupssd.1
 |-  ( ph -> B C_ C )
2 xrsupssd.2
 |-  ( ph -> C C_ RR* )
3 xrltso
 |-  < Or RR*
4 3 a1i
 |-  ( ph -> < Or RR* )
5 1 2 sstrd
 |-  ( ph -> B C_ RR* )
6 xrsupss
 |-  ( B C_ RR* -> E. x e. RR* ( A. y e. B -. x < y /\ A. y e. RR* ( y < x -> E. z e. B y < z ) ) )
7 5 6 syl
 |-  ( ph -> E. x e. RR* ( A. y e. B -. x < y /\ A. y e. RR* ( y < x -> E. z e. B y < z ) ) )
8 xrsupss
 |-  ( C C_ RR* -> E. x e. RR* ( A. y e. C -. x < y /\ A. y e. RR* ( y < x -> E. z e. C y < z ) ) )
9 2 8 syl
 |-  ( ph -> E. x e. RR* ( A. y e. C -. x < y /\ A. y e. RR* ( y < x -> E. z e. C y < z ) ) )
10 4 1 2 7 9 supssd
 |-  ( ph -> -. sup ( C , RR* , < ) < sup ( B , RR* , < ) )
11 4 7 supcl
 |-  ( ph -> sup ( B , RR* , < ) e. RR* )
12 4 9 supcl
 |-  ( ph -> sup ( C , RR* , < ) e. RR* )
13 xrlenlt
 |-  ( ( sup ( B , RR* , < ) e. RR* /\ sup ( C , RR* , < ) e. RR* ) -> ( sup ( B , RR* , < ) <_ sup ( C , RR* , < ) <-> -. sup ( C , RR* , < ) < sup ( B , RR* , < ) ) )
14 11 12 13 syl2anc
 |-  ( ph -> ( sup ( B , RR* , < ) <_ sup ( C , RR* , < ) <-> -. sup ( C , RR* , < ) < sup ( B , RR* , < ) ) )
15 10 14 mpbird
 |-  ( ph -> sup ( B , RR* , < ) <_ sup ( C , RR* , < ) )