Theorem derangen2

Description: Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-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	derangen2	|- ( A e. Fin -> ( D ` A ) = ( S ` ( # ` A ) ) )

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		hashcl	|- ( A e. Fin -> ( # ` A ) e. NN0 )
4	1 2	subfacval	|- ( ( # ` A ) e. NN0 -> ( S ` ( # ` A ) ) = ( D ` ( 1 ... ( # ` A ) ) ) )
5	3 4	syl	|- ( A e. Fin -> ( S ` ( # ` A ) ) = ( D ` ( 1 ... ( # ` A ) ) ) )
6		hashfz1	|- ( ( # ` A ) e. NN0 -> ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) )
7	3 6	syl	|- ( A e. Fin -> ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) )
8		fzfid	|- ( A e. Fin -> ( 1 ... ( # ` A ) ) e. Fin )
9		hashen	|- ( ( ( 1 ... ( # ` A ) ) e. Fin /\ A e. Fin ) -> ( ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) <-> ( 1 ... ( # ` A ) ) ~~ A ) )
10	8 9	mpancom	|- ( A e. Fin -> ( ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) <-> ( 1 ... ( # ` A ) ) ~~ A ) )
11	7 10	mpbid	|- ( A e. Fin -> ( 1 ... ( # ` A ) ) ~~ A )
12	1	derangen	|- ( ( ( 1 ... ( # ` A ) ) ~~ A /\ A e. Fin ) -> ( D ` ( 1 ... ( # ` A ) ) ) = ( D ` A ) )
13	11 12	mpancom	|- ( A e. Fin -> ( D ` ( 1 ... ( # ` A ) ) ) = ( D ` A ) )
14	5 13	eqtr2d	|- ( A e. Fin -> ( D ` A ) = ( S ` ( # ` A ) ) )