Metamath Proof Explorer

Theorem supxr

Description: The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006) (Revised by Mario Carneiro, 21-Apr-2015)

Ref Expression
Assertion supxr 
|- ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> sup ( A , RR* , < ) = B )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> B e. RR* )
2 simprl 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> A. x e. A -. B < x )
3 xrub 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) <-> A. x e. RR* ( x < B -> E. y e. A x < y ) ) )
4 3 biimpa 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) -> A. x e. RR* ( x < B -> E. y e. A x < y ) )
5 4 adantrl 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> A. x e. RR* ( x < B -> E. y e. A x < y ) )
6 xrltso 
 |-  < Or RR*
7 6 a1i 
 |-  ( T. -> < Or RR* )
8 7 eqsup 
 |-  ( T. -> ( ( B e. RR* /\ A. x e. A -. B < x /\ A. x e. RR* ( x < B -> E. y e. A x < y ) ) -> sup ( A , RR* , < ) = B ) )
9 8 mptru 
 |-  ( ( B e. RR* /\ A. x e. A -. B < x /\ A. x e. RR* ( x < B -> E. y e. A x < y ) ) -> sup ( A , RR* , < ) = B )
10 1 2 5 9 syl3anc 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> sup ( A , RR* , < ) = B )