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*BABsupA*<

Proof

Step Hyp Ref Expression
1 ssel2 A*BAB*
2 supxrcl A*supA*<*
3 2 adantr A*BAsupA*<*
4 xrltso <Or*
5 4 a1i A*<Or*
6 xrsupss A*x*yA¬x<yy*y<xzAy<z
7 5 6 supub A*BA¬supA*<<B
8 7 imp A*BA¬supA*<<B
9 1 3 8 xrnltled A*BABsupA*<