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 e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
Assertion derangsn 
|- ( A e. V -> ( D ` { A } ) = 0 )

Proof

Step Hyp Ref Expression
1 derang.d 
 |-  D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2 snfi 
 |-  { A } e. Fin
3 1 derangval 
 |-  ( { A } e. Fin -> ( D ` { A } ) = ( # ` { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } ) )
4 2 3 ax-mp 
 |-  ( D ` { A } ) = ( # ` { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } )
5 f1of 
 |-  ( f : { A } -1-1-onto-> { A } -> f : { A } --> { A } )
6 5 adantr 
 |-  ( ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) -> f : { A } --> { A } )
7 snidg 
 |-  ( A e. V -> A e. { A } )
8 ffvelrn 
 |-  ( ( f : { A } --> { A } /\ A e. { A } ) -> ( f ` A ) e. { A } )
9 6 7 8 syl2anr 
 |-  ( ( A e. V /\ ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) ) -> ( f ` A ) e. { A } )
10 simpr 
 |-  ( ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) -> A. y e. { 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 e. { A } /\ A. y e. { A } ( f ` y ) =/= y ) -> ( f ` A ) =/= A )
15 7 10 14 syl2an 
 |-  ( ( A e. V /\ ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) ) -> ( f ` A ) =/= A )
16 nelsn 
 |-  ( ( f ` A ) =/= A -> -. ( f ` A ) e. { A } )
17 15 16 syl 
 |-  ( ( A e. V /\ ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) ) -> -. ( f ` A ) e. { A } )
18 9 17 pm2.21dd 
 |-  ( ( A e. V /\ ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) ) -> f e. (/) )
19 18 ex 
 |-  ( A e. V -> ( ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) -> f e. (/) ) )
20 19 abssdv 
 |-  ( A e. V -> { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } C_ (/) )
21 ss0 
 |-  ( { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } C_ (/) -> { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } = (/) )
22 20 21 syl 
 |-  ( A e. V -> { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } = (/) )
23 22 fveq2d 
 |-  ( A e. V -> ( # ` { f | ( f : { A } -1-1-onto-> { A } /\ A. y e. { A } ( f ` y ) =/= y ) } ) = ( # ` (/) ) )
24 4 23 syl5eq 
 |-  ( A e. V -> ( D ` { A } ) = ( # ` (/) ) )
25 hash0 
 |-  ( # ` (/) ) = 0
26 24 25 eqtrdi 
 |-  ( A e. V -> ( D ` { A } ) = 0 )