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	$$⊢\phi \to M\in \mathbb{Z}$$
	uzidd2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzidd2	$$⊢\phi \to M\in Z$$

Proof

Step	Hyp	Ref	Expression
1		uzidd2.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzidd2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3	1	uzidd	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
4	3 2	eleqtrrdi	$$⊢\phi \to M\in Z$$