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