Metamath Proof Explorer

Theorem infxrcl

Description: The infimum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 19-Jan-2006) (Revised by AV, 5-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 1 a1i 
 |-  ( A C_ RR* -> < Or RR* )
3 xrinfmss 
 |-  ( A C_ RR* -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
4 2 3 infcl 
 |-  ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )