Metamath Proof Explorer


Theorem subfac0

Description: The subfactorial at zero. (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 subfac0 S 0 = 1

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 0nn0 0 0
4 1 2 subfacval 0 0 S 0 = D 1 0
5 3 4 ax-mp S 0 = D 1 0
6 fz10 1 0 =
7 6 fveq2i D 1 0 = D
8 1 derang0 D = 1
9 5 7 8 3eqtri S 0 = 1