Theorem subfac1

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

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		1nn0	|- 1 e. NN0
4	1 2	subfacval	|- ( 1 e. NN0 -> ( S ` 1 ) = ( D ` ( 1 ... 1 ) ) )
5	3 4	ax-mp	|- ( S ` 1 ) = ( D ` ( 1 ... 1 ) )
6		1z	|- 1 e. ZZ
7		fzsn	|- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
8	6 7	ax-mp	|- ( 1 ... 1 ) = { 1 }
9	8	fveq2i	|- ( D ` ( 1 ... 1 ) ) = ( D ` { 1 } )
10	1	derangsn	|- ( 1 e. NN0 -> ( D ` { 1 } ) = 0 )
11	3 10	ax-mp	|- ( D ` { 1 } ) = 0
12	5 9 11	3eqtri	|- ( S ` 1 ) = 0