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* , < ) )