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 = ( 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	subfacval	|- ( N e. NN0 -> ( S ` N ) = ( D ` ( 1 ... N ) ) )

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		oveq2	|- ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
4	3	fveq2d	|- ( n = N -> ( D ` ( 1 ... n ) ) = ( D ` ( 1 ... N ) ) )
5		fvex	|- ( D ` ( 1 ... N ) ) e. _V
6	4 2 5	fvmpt	|- ( N e. NN0 -> ( S ` N ) = ( D ` ( 1 ... N ) ) )