Theorem nn0uz

Description: Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005)

	Ref	Expression
Assertion	nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$

Proof

Step	Hyp	Ref	Expression
1		nn0zrab	$$⊢{\mathbb{N}}_0=\left\{k\in \mathbb{Z}|0\le k\right\}$$
2		0z	$$⊢0\in \mathbb{Z}$$
3		uzval	$$⊢0\in \mathbb{Z}\to {\mathbb{Z}}_{\ge 0}=\left\{k\in \mathbb{Z}|0\le k\right\}$$
4	2 3	ax-mp	$$⊢{\mathbb{Z}}_{\ge 0}=\left\{k\in \mathbb{Z}|0\le k\right\}$$
5	1 4	eqtr4i	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$