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 = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
	subfac.n	|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
Assertion	subfacf	|- S : NN0 --> NN0

Proof

Step	Hyp	Ref	Expression
1		derang.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2		subfac.n	|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3		fzfi	|- ( 1 ... n ) e. Fin
4	1	derangf	|- D : Fin --> NN0
5	4	ffvelcdmi	|- ( ( 1 ... n ) e. Fin -> ( D ` ( 1 ... n ) ) e. NN0 )
6	3 5	ax-mp	|- ( D ` ( 1 ... n ) ) e. NN0
7	6	rgenw	|- A. n e. NN0 ( D ` ( 1 ... n ) ) e. NN0
8	2	fmpt	|- ( A. n e. NN0 ( D ` ( 1 ... n ) ) e. NN0 <-> S : NN0 --> NN0 )
9	7 8	mpbi	|- S : NN0 --> NN0