Theorem derangf

Description: The derangement number is a function from finite sets to nonnegative integers. (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	derangf	|- D : Fin --> 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		deranglem	|- ( x e. Fin -> { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } e. Fin )
3		hashcl	|- ( { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } e. Fin -> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) e. NN0 )
4	2 3	syl	|- ( x e. Fin -> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) e. NN0 )
5	1 4	fmpti	|- D : Fin --> NN0