Metamath Proof Explorer


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 ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )