Metamath Proof Explorer

Theorem supxrcl

Description: The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005)

Ref Expression
Assertion supxrcl 
|- ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 1 a1i 
 |-  ( A C_ RR* -> < Or RR* )
3 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 ) ) )
4 2 3 supcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )