Theorem subfac0

Description: The subfactorial at zero. (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	subfac0	$$⊢S\left(0\right)=1$$

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		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	1 2	subfacval	$$⊢0\in {\mathbb{N}}_0\to S\left(0\right)=D\left(\left(1\dots 0\right)\right)$$
5	3 4	ax-mp	$$⊢S\left(0\right)=D\left(\left(1\dots 0\right)\right)$$
6		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
7	6	fveq2i	$$⊢D\left(\left(1\dots 0\right)\right)=D\left(\varnothing \right)$$
8	1	derang0	$$⊢D\left(\varnothing \right)=1$$
9	5 7 8	3eqtri	$$⊢S\left(0\right)=1$$