Theorem subfac0

Description: The subfactorial at zero. (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	subfac0	|- ( S ` 0 ) = 1

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		0nn0	|- 0 e. NN0
4	1 2	subfacval	|- ( 0 e. NN0 -> ( S ` 0 ) = ( D ` ( 1 ... 0 ) ) )
5	3 4	ax-mp	|- ( S ` 0 ) = ( D ` ( 1 ... 0 ) )
6		fz10	|- ( 1 ... 0 ) = (/)
7	6	fveq2i	|- ( D ` ( 1 ... 0 ) ) = ( D ` (/) )
8	1	derang0	|- ( D ` (/) ) = 1
9	5 7 8	3eqtri	|- ( S ` 0 ) = 1