Theorem subfacf

Description: The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
	subfac.n	$$⊢S=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)$$
Assertion	subfacf	$$⊢S:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
2		subfac.n	$$⊢S=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)$$
3		fzfi	$$⊢\left(1\dots n\right)\in \mathrm{Fin}$$
4	1	derangf	$$⊢D:\mathrm{Fin}⟶{\mathbb{N}}_0$$
5	4	ffvelcdmi	$$⊢\left(1\dots n\right)\in \mathrm{Fin}\to D\left(\left(1\dots n\right)\right)\in {\mathbb{N}}_0$$
6	3 5	ax-mp	$$⊢D\left(\left(1\dots n\right)\right)\in {\mathbb{N}}_0$$
7	6	rgenw	$$⊢\forall n\in {\mathbb{N}}_{0}D\left(\left(1\dots n\right)\right)\in {\mathbb{N}}_0$$
8	2	fmpt	$$⊢\forall n\in {\mathbb{N}}_{0}D\left(\left(1\dots n\right)\right)\in {\mathbb{N}}_0\leftrightarrow S:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
9	7 8	mpbi	$$⊢S:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$