Theorem eluzel2

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathrm{dom}{\mathbb{Z}}_{\ge }$$
2		uzf	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$
3	2	fdmi	$$⊢\mathrm{dom}{\mathbb{Z}}_{\ge }=\mathbb{Z}$$
4	1 3	eleqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$