Metamath Proof Explorer

Theorem supxrss

Description: Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion supxrss 
|- ( ( A C_ B /\ B C_ RR* ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A C_ B /\ B C_ RR* ) /\ x e. A ) -> B C_ RR* )
2 simpl 
 |-  ( ( A C_ B /\ B C_ RR* ) -> A C_ B )
3 2 sselda 
 |-  ( ( ( A C_ B /\ B C_ RR* ) /\ x e. A ) -> x e. B )
4 supxrub 
 |-  ( ( B C_ RR* /\ x e. B ) -> x <_ sup ( B , RR* , < ) )
5 1 3 4 syl2anc 
 |-  ( ( ( A C_ B /\ B C_ RR* ) /\ x e. A ) -> x <_ sup ( B , RR* , < ) )
6 5 ralrimiva 
 |-  ( ( A C_ B /\ B C_ RR* ) -> A. x e. A x <_ sup ( B , RR* , < ) )
7 sstr 
 |-  ( ( A C_ B /\ B C_ RR* ) -> A C_ RR* )
8 supxrcl 
 |-  ( B C_ RR* -> sup ( B , RR* , < ) e. RR* )
9 8 adantl 
 |-  ( ( A C_ B /\ B C_ RR* ) -> sup ( B , RR* , < ) e. RR* )
10 supxrleub 
 |-  ( ( A C_ RR* /\ sup ( B , RR* , < ) e. RR* ) -> ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) <-> A. x e. A x <_ sup ( B , RR* , < ) ) )
11 7 9 10 syl2anc 
 |-  ( ( A C_ B /\ B C_ RR* ) -> ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) <-> A. x e. A x <_ sup ( B , RR* , < ) ) )
12 6 11 mpbird 
 |-  ( ( A C_ B /\ B C_ RR* ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )