Metamath Proof Explorer


Theorem infssuzle

Description: The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infssuzle
|- ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> inf ( S , RR , < ) <_ A )

Proof

Step Hyp Ref Expression
1 ne0i
 |-  ( A e. S -> S =/= (/) )
2 uzwo
 |-  ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k )
3 1 2 sylan2
 |-  ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> E. j e. S A. k e. S j <_ k )
4 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
5 zssre
 |-  ZZ C_ RR
6 4 5 sstri
 |-  ( ZZ>= ` M ) C_ RR
7 sstr
 |-  ( ( S C_ ( ZZ>= ` M ) /\ ( ZZ>= ` M ) C_ RR ) -> S C_ RR )
8 6 7 mpan2
 |-  ( S C_ ( ZZ>= ` M ) -> S C_ RR )
9 lbinfle
 |-  ( ( S C_ RR /\ E. j e. S A. k e. S j <_ k /\ A e. S ) -> inf ( S , RR , < ) <_ A )
10 9 3com23
 |-  ( ( S C_ RR /\ A e. S /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) <_ A )
11 8 10 syl3an1
 |-  ( ( S C_ ( ZZ>= ` M ) /\ A e. S /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) <_ A )
12 3 11 mpd3an3
 |-  ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> inf ( S , RR , < ) <_ A )