Metamath Proof Explorer


Theorem lbinf

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

Ref Expression
Assertion lbinf SxSySxysupS<=ιxS|ySxy

Proof

Step Hyp Ref Expression
1 ltso <Or
2 1 a1i SxSySxy<Or
3 lbcl SxSySxyιxS|ySxyS
4 ssel SιxS|ySxySιxS|ySxy
5 4 adantr SxSySxyιxS|ySxySιxS|ySxy
6 3 5 mpd SxSySxyιxS|ySxy
7 6 adantr SxSySxyzSιxS|ySxy
8 ssel2 SzSz
9 8 adantlr SxSySxyzSz
10 lble SxSySxyzSιxS|ySxyz
11 10 3expa SxSySxyzSιxS|ySxyz
12 7 9 11 lensymd SxSySxyzS¬z<ιxS|ySxy
13 2 6 3 12 infmin SxSySxysupS<=ιxS|ySxy