Metamath Proof Explorer

Theorem subfaclefac

Description: The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses derang.d 
|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
subfac.n 
|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
Assertion subfaclefac 
|- ( N e. NN0 -> ( S ` N ) <_ ( ! ` N ) )

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 subfac.n 
 |-  S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3 anidm 
 |-  ( ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) <-> f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
4 3 abbii 
 |-  { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) } = { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }
5 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
6 deranglem 
 |-  ( ( 1 ... N ) e. Fin -> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) } e. Fin )
7 5 6 syl 
 |-  ( N e. NN0 -> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) } e. Fin )
8 4 7 eqeltrrid 
 |-  ( N e. NN0 -> { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin )
9 simpl 
 |-  ( ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) -> f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
10 9 ss2abi 
 |-  { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } C_ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }
11 ssdomg 
 |-  ( { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin -> ( { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } C_ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } -> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ~<_ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
12 8 10 11 mpisyl 
 |-  ( N e. NN0 -> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ~<_ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
13 deranglem 
 |-  ( ( 1 ... N ) e. Fin -> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } e. Fin )
14 5 13 syl 
 |-  ( N e. NN0 -> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } e. Fin )
15 hashdom 
 |-  ( ( { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin ) -> ( ( # ` { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ) <_ ( # ` { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) <-> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ~<_ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
16 14 8 15 syl2anc 
 |-  ( N e. NN0 -> ( ( # ` { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ) <_ ( # ` { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) <-> { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ~<_ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
17 12 16 mpbird 
 |-  ( N e. NN0 -> ( # ` { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ) <_ ( # ` { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
18 1 2 subfacval 
 |-  ( N e. NN0 -> ( S ` N ) = ( D ` ( 1 ... N ) ) )
19 1 derangval 
 |-  ( ( 1 ... N ) e. Fin -> ( D ` ( 1 ... N ) ) = ( # ` { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ) )
20 5 19 syl 
 |-  ( N e. NN0 -> ( D ` ( 1 ... N ) ) = ( # ` { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ) )
21 18 20 eqtrd 
 |-  ( N e. NN0 -> ( S ` N ) = ( # ` { f | ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ A. y e. ( 1 ... N ) ( f ` y ) =/= y ) } ) )
22 hashfac 
 |-  ( ( 1 ... N ) e. Fin -> ( # ` { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) = ( ! ` ( # ` ( 1 ... N ) ) ) )
23 5 22 syl 
 |-  ( N e. NN0 -> ( # ` { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) = ( ! ` ( # ` ( 1 ... N ) ) ) )
24 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
25 24 fveq2d 
 |-  ( N e. NN0 -> ( ! ` ( # ` ( 1 ... N ) ) ) = ( ! ` N ) )
26 23 25 eqtr2d 
 |-  ( N e. NN0 -> ( ! ` N ) = ( # ` { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
27 17 21 26 3brtr4d 
 |-  ( N e. NN0 -> ( S ` N ) <_ ( ! ` N ) )