Metamath Proof Explorer


Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion supxrleub A*B*supA*<BxAxB

Proof

Step Hyp Ref Expression
1 supxrlub A*B*B<supA*<xAB<x
2 1 notbid A*B*¬B<supA*<¬xAB<x
3 ralnex xA¬B<x¬xAB<x
4 2 3 bitr4di A*B*¬B<supA*<xA¬B<x
5 supxrcl A*supA*<*
6 xrlenlt supA*<*B*supA*<B¬B<supA*<
7 5 6 sylan A*B*supA*<B¬B<supA*<
8 simpl A*B*A*
9 8 sselda A*B*xAx*
10 simplr A*B*xAB*
11 9 10 xrlenltd A*B*xAxB¬B<x
12 11 ralbidva A*B*xAxBxA¬B<x
13 4 7 12 3bitr4d A*B*supA*<BxAxB