Theorem uzid3

Description: Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	uzid3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzid3	$$⊢N\in Z\to N\in {\mathbb{Z}}_{\ge N}$$

Proof

Step	Hyp	Ref	Expression
1		uzid3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2	1	eleq2i	$$⊢N\in Z\leftrightarrow N\in {\mathbb{Z}}_{\ge M}$$
3	2	biimpi	$$⊢N\in Z\to N\in {\mathbb{Z}}_{\ge M}$$
4		uzid2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in {\mathbb{Z}}_{\ge N}$$
5	3 4	syl	$$⊢N\in Z\to N\in {\mathbb{Z}}_{\ge N}$$