Theorem uzval

Description: The value of the upper integers function. (Contributed by NM, 5-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	uzval	$$⊢N\in \mathbb{Z}\to {\mathbb{Z}}_{\ge N}=\left\{k\in \mathbb{Z}|N\le k\right\}$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢j=N\to \left(j\le k\leftrightarrow N\le k\right)$$
2	1	rabbidv	$$⊢j=N\to \left\{k\in \mathbb{Z}|j\le k\right\}=\left\{k\in \mathbb{Z}|N\le k\right\}$$
3		df-uz	$$⊢{\mathbb{Z}}_{\ge }=\left(j\in \mathbb{Z}⟼\left\{k\in \mathbb{Z}|j\le k\right\}\right)$$
4		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
5	4	rabex	$$⊢\left\{k\in \mathbb{Z}|N\le k\right\}\in \mathrm{V}$$
6	2 3 5	fvmpt	$$⊢N\in \mathbb{Z}\to {\mathbb{Z}}_{\ge N}=\left\{k\in \mathbb{Z}|N\le k\right\}$$