Metamath Proof Explorer


Theorem subfac1

Description: The subfactorial at one. (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 subfac1 S 1 = 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 1nn0 1 0
4 1 2 subfacval 1 0 S 1 = D 1 1
5 3 4 ax-mp S 1 = D 1 1
6 1z 1
7 fzsn 1 1 1 = 1
8 6 7 ax-mp 1 1 = 1
9 8 fveq2i D 1 1 = D 1
10 1 derangsn 1 0 D 1 = 0
11 3 10 ax-mp D 1 = 0
12 5 9 11 3eqtri S 1 = 0