Theorem prednn0

Description: The value of the predecessor class over NN0 . (Contributed by Scott Fenton, 9-May-2014)

	Ref	Expression
Assertion	prednn0	$$⊢N\in {\mathbb{N}}_0\to Pred\left(<,{\mathbb{N}}_0,N\right)=\left(0\dots N-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		predeq2	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}\to Pred\left(<,{\mathbb{N}}_0,N\right)=Pred\left(<,{\mathbb{Z}}_{\ge 0},N\right)$$
3	1 2	ax-mp	$$⊢Pred\left(<,{\mathbb{N}}_0,N\right)=Pred\left(<,{\mathbb{Z}}_{\ge 0},N\right)$$
4		preduz	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to Pred\left(<,{\mathbb{Z}}_{\ge 0},N\right)=\left(0\dots N-1\right)$$
5	3 4	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to Pred\left(<,{\mathbb{N}}_0,N\right)=\left(0\dots N-1\right)$$
6	5 1	eleq2s	$$⊢N\in {\mathbb{N}}_0\to Pred\left(<,{\mathbb{N}}_0,N\right)=\left(0\dots N-1\right)$$