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 )