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 Fin f | f : x 1-1 onto x y x f y y
subfac.n S = n 0 D 1 n
Assertion subfacval N 0 S N = D 1 N

Proof

Step Hyp Ref Expression
1 derang.d D = x Fin f | f : x 1-1 onto x y x f y y
2 subfac.n S = n 0 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 V
6 4 2 5 fvmpt N 0 S N = D 1 N