Metamath Proof Explorer


Theorem derangsn

Description: The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis derang.d D = x Fin f | f : x 1-1 onto x y x f y y
Assertion derangsn A V D A = 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 snfi A Fin
3 1 derangval A Fin D A = f | f : A 1-1 onto A y A f y y
4 2 3 ax-mp D A = f | f : A 1-1 onto A y A f y y
5 f1of f : A 1-1 onto A f : A A
6 5 adantr f : A 1-1 onto A y A f y y f : A A
7 snidg A V A A
8 ffvelrn f : A A A A f A A
9 6 7 8 syl2anr A V f : A 1-1 onto A y A f y y f A A
10 simpr f : A 1-1 onto A y A f y y y A f y y
11 fveq2 y = A f y = f A
12 id y = A y = A
13 11 12 neeq12d y = A f y y f A A
14 13 rspcva A A y A f y y f A A
15 7 10 14 syl2an A V f : A 1-1 onto A y A f y y f A A
16 nelsn f A A ¬ f A A
17 15 16 syl A V f : A 1-1 onto A y A f y y ¬ f A A
18 9 17 pm2.21dd A V f : A 1-1 onto A y A f y y f
19 18 ex A V f : A 1-1 onto A y A f y y f
20 19 abssdv A V f | f : A 1-1 onto A y A f y y
21 ss0 f | f : A 1-1 onto A y A f y y f | f : A 1-1 onto A y A f y y =
22 20 21 syl A V f | f : A 1-1 onto A y A f y y =
23 22 fveq2d A V f | f : A 1-1 onto A y A f y y =
24 4 23 syl5eq A V D A =
25 hash0 = 0
26 24 25 eqtrdi A V D A = 0