Metamath Proof Explorer

Theorem subfacp1

Description: A two-term recurrence for the subfactorial. This theorem allows 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 bitrid 
 |-  ( 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 ) ) ) ) )