Theorem derangval

Description: Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypothesis	derang.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
Assertion	derangval	|- ( A e. Fin -> ( D ` A ) = ( # ` { f | ( f : A -1-1-onto-> A /\ A. y e. A ( f ` y ) =/= y ) } ) )

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		f1oeq2	|- ( x = A -> ( f : x -1-1-onto-> x <-> f : A -1-1-onto-> x ) )
3		f1oeq3	|- ( x = A -> ( f : A -1-1-onto-> x <-> f : A -1-1-onto-> A ) )
4	2 3	bitrd	|- ( x = A -> ( f : x -1-1-onto-> x <-> f : A -1-1-onto-> A ) )
5		raleq	|- ( x = A -> ( A. y e. x ( f ` y ) =/= y <-> A. y e. A ( f ` y ) =/= y ) )
6	4 5	anbi12d	|- ( x = A -> ( ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) <-> ( f : A -1-1-onto-> A /\ A. y e. A ( f ` y ) =/= y ) ) )
7	6	abbidv	|- ( x = A -> { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } = { f | ( f : A -1-1-onto-> A /\ A. y e. A ( f ` y ) =/= y ) } )
8	7	fveq2d	|- ( x = A -> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) = ( # ` { f | ( f : A -1-1-onto-> A /\ A. y e. A ( f ` y ) =/= y ) } ) )
9		fvex	|- ( # ` { f | ( f : A -1-1-onto-> A /\ A. y e. A ( f ` y ) =/= y ) } ) e. _V
10	8 1 9	fvmpt	|- ( A e. Fin -> ( D ` A ) = ( # ` { f | ( f : A -1-1-onto-> A /\ A. y e. A ( f ` y ) =/= y ) } ) )