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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ dom ℤ≥ )
2		uzf	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
3	2	fdmi	⊢ dom ℤ≥ = ℤ
4	1 3	eleqtrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )