Theorem subfacval

Description: The subfactorial is defined as the number of derangements (see derangval ) of the set ( 1 ... N ) . (Contributed by Mario Carneiro, 21-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	subfacval	$$⊢N\in {\mathbb{N}}_0\to S\left(N\right)=D\left(\left(1\dots N\right)\right)$$

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		oveq2	$$⊢n=N\to \left(1\dots n\right)=\left(1\dots N\right)$$
4	3	fveq2d	$$⊢n=N\to D\left(\left(1\dots n\right)\right)=D\left(\left(1\dots N\right)\right)$$
5		fvex	$$⊢D\left(\left(1\dots N\right)\right)\in \mathrm{V}$$
6	4 2 5	fvmpt	$$⊢N\in {\mathbb{N}}_0\to S\left(N\right)=D\left(\left(1\dots N\right)\right)$$