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 C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> inf ( S , RR , < ) e. S )

Proof

Step	Hyp	Ref	Expression
1		uzssz	|- ( ZZ>= ` M ) C_ ZZ
2		zssre	|- ZZ C_ RR
3	1 2	sstri	|- ( ZZ>= ` M ) C_ RR
4		sstr	|- ( ( S C_ ( ZZ>= ` M ) /\ ( ZZ>= ` M ) C_ RR ) -> S C_ RR )
5	3 4	mpan2	|- ( S C_ ( ZZ>= ` M ) -> S C_ RR )
6		uzwo	|- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k )
7		lbinfcl	|- ( ( S C_ RR /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) e. S )
8	5 6 7	syl2an2r	|- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> inf ( S , RR , < ) e. S )