Theorem subfac1

Description: The subfactorial at one. (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	subfac1	$$⊢S\left(1\right)=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		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4	1 2	subfacval	$$⊢1\in {\mathbb{N}}_0\to S\left(1\right)=D\left(\left(1\dots 1\right)\right)$$
5	3 4	ax-mp	$$⊢S\left(1\right)=D\left(\left(1\dots 1\right)\right)$$
6		1z	$$⊢1\in \mathbb{Z}$$
7		fzsn	$$⊢1\in \mathbb{Z}\to \left(1\dots 1\right)=\left\{1\right\}$$
8	6 7	ax-mp	$$⊢\left(1\dots 1\right)=\left\{1\right\}$$
9	8	fveq2i	$$⊢D\left(\left(1\dots 1\right)\right)=D\left(\left\{1\right\}\right)$$
10	1	derangsn	$$⊢1\in {\mathbb{N}}_0\to D\left(\left\{1\right\}\right)=0$$
11	3 10	ax-mp	$$⊢D\left(\left\{1\right\}\right)=0$$
12	5 9 11	3eqtri	$$⊢S\left(1\right)=0$$