Metamath Proof Explorer


Theorem subfacval

Description: The subfactorial is defined as the number of derangements (see derangval ) of the set ( 1 ... N ) . (Contributed by Mario Carneiro, 21-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 subfacval
|- ( N e. NN0 -> ( S ` N ) = ( D ` ( 1 ... N ) ) )

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 oveq2
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
4 3 fveq2d
 |-  ( n = N -> ( D ` ( 1 ... n ) ) = ( D ` ( 1 ... N ) ) )
5 fvex
 |-  ( D ` ( 1 ... N ) ) e. _V
6 4 2 5 fvmpt
 |-  ( N e. NN0 -> ( S ` N ) = ( D ` ( 1 ... N ) ) )