Metamath Proof Explorer


Theorem lbinfcl

Description: If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion lbinfcl SxSySxyinfS<S

Proof

Step Hyp Ref Expression
1 lbinf SxSySxyinfS<=ιxS|ySxy
2 lbcl SxSySxyιxS|ySxyS
3 1 2 eqeltrd SxSySxyinfS<S