Theorem uzidd2

Description: Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	uzidd2.1	|- ( ph -> M e. ZZ )
	uzidd2.2	|- Z = ( ZZ>= ` M )
Assertion	uzidd2	|- ( ph -> M e. Z )

Proof

Step	Hyp	Ref	Expression
1		uzidd2.1	|- ( ph -> M e. ZZ )
2		uzidd2.2	|- Z = ( ZZ>= ` M )
3	1	uzidd	|- ( ph -> M e. ( ZZ>= ` M ) )
4	3 2	eleqtrrdi	|- ( ph -> M e. Z )