Theorem subfacp1

Description: A two-term recurrence for the subfactorial. This theorem allows us to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 , subfac1 . (Contributed by Mario Carneiro, 23-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	subfacp1	|- ( N e. NN -> ( S ` ( N + 1 ) ) = ( N x. ( ( S ` N ) + ( S ` ( N - 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		f1oeq1	|- ( g = f -> ( g : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
4		fveq2	|- ( z = y -> ( g ` z ) = ( g ` y ) )
5		id	|- ( z = y -> z = y )
6	4 5	neeq12d	|- ( z = y -> ( ( g ` z ) =/= z <-> ( g ` y ) =/= y ) )
7	6	cbvralvw	|- ( A. z e. ( 1 ... ( N + 1 ) ) ( g ` z ) =/= z <-> A. y e. ( 1 ... ( N + 1 ) ) ( g ` y ) =/= y )
8		fveq1	|- ( g = f -> ( g ` y ) = ( f ` y ) )
9	8	neeq1d	|- ( g = f -> ( ( g ` y ) =/= y <-> ( f ` y ) =/= y ) )
10	9	ralbidv	|- ( g = f -> ( A. y e. ( 1 ... ( N + 1 ) ) ( g ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) )
11	7 10	syl5bb	|- ( g = f -> ( A. z e. ( 1 ... ( N + 1 ) ) ( g ` z ) =/= z <-> A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) )
12	3 11	anbi12d	|- ( g = f -> ( ( g : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. z e. ( 1 ... ( N + 1 ) ) ( g ` z ) =/= z ) <-> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) ) )
13	12	cbvabv	|- { g | ( g : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. z e. ( 1 ... ( N + 1 ) ) ( g ` z ) =/= z ) } = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
14	1 2 13	subfacp1lem6	|- ( N e. NN -> ( S ` ( N + 1 ) ) = ( N x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )