This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supxrub

Description: A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 ssel2 
 |-  ( ( A C_ RR* /\ B e. A ) -> B e. RR* )
2 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
3 2 adantr 
 |-  ( ( A C_ RR* /\ B e. A ) -> sup ( A , RR* , < ) e. RR* )
4 xrltso 
 |-  < Or RR*
5 4 a1i 
 |-  ( A C_ RR* -> < Or RR* )
6 xrsupss 
 |-  ( A C_ RR* -> E. x e. RR* ( A. y e. A -. x < y /\ A. y e. RR* ( y < x -> E. z e. A y < z ) ) )
7 5 6 supub 
 |-  ( A C_ RR* -> ( B e. A -> -. sup ( A , RR* , < ) < B ) )
8 7 imp 
 |-  ( ( A C_ RR* /\ B e. A ) -> -. sup ( A , RR* , < ) < B )
9 1 3 8 xrnltled 
 |-  ( ( A C_ RR* /\ B e. A ) -> B <_ sup ( A , RR* , < ) )