Metamath Proof Explorer


Theorem subfacf

Description: The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-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 subfacf S : 0 0

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 fzfi 1 n Fin
4 1 derangf D : Fin 0
5 4 ffvelrni 1 n Fin D 1 n 0
6 3 5 ax-mp D 1 n 0
7 6 rgenw n 0 D 1 n 0
8 2 fmpt n 0 D 1 n 0 S : 0 0
9 7 8 mpbi S : 0 0