Theorem uzid

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005)

	Ref	Expression
Assertion	uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℤ )
2		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
3	2	leidd	⊢ ( 𝑀 ∈ ℤ → 𝑀 ≤ 𝑀 )
4		eluz1	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ) ) )
5	1 3 4	mpbir2and	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )