Theorem prednn

Description: The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013)

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

Proof

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