Metamath Proof Explorer

Theorem infssuzcl

Description: The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infssuzcl S M S sup S < S


Step Hyp Ref Expression
1 uzssz M
2 zssre
3 1 2 sstri M
4 sstr S M M S
5 3 4 mpan2 S M S
6 uzwo S M S j S k S j k
7 lbinfcl S j S k S j k sup S < S
8 5 6 7 syl2an2r S M S sup S < S