Metamath Proof Explorer

Theorem supxr2

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

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

Proof

Step Hyp Ref Expression
1 ssel2 
 |-  ( ( A C_ RR* /\ x e. A ) -> x e. RR* )
2 xrlenlt 
 |-  ( ( x e. RR* /\ B e. RR* ) -> ( x <_ B <-> -. B < x ) )
3 1 2 sylan 
 |-  ( ( ( A C_ RR* /\ x e. A ) /\ B e. RR* ) -> ( x <_ B <-> -. B < x ) )
4 3 an32s 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> ( x <_ B <-> -. B < x ) )
5 4 ralbidva 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. A x <_ B <-> A. x e. A -. B < x ) )
6 5 anbi1d 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( ( A. x e. A x <_ B /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) <-> ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) )
7 6 biimpa 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A x <_ B /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> ( A. x e. A -. B < x /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) )
8 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 )
9 7 8 syldan 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ ( A. x e. A x <_ B /\ A. x e. RR ( x < B -> E. y e. A x < y ) ) ) -> sup ( A , RR* , < ) = B )