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	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$

Step	Hyp	Ref	Expression
1		id	$⊢ M \in ℤ \to M \in ℤ$
2		zre	$⊢ M \in ℤ \to M \in ℝ$
3	2	leidd	$⊢ M \in ℤ \to M \leq M$
4		eluz1	$⊢ M \in ℤ \to (M \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land M \leq M))$
5	1 3 4	mpbir2and	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$