Theorem derang0

Description: The derangement number of the empty set. (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	derang0	|- ( D ` (/) ) = 1

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		0fin	|- (/) e. Fin
3	1	derangval	|- ( (/) e. Fin -> ( D ` (/) ) = ( # ` { f | ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) } ) )
4	2 3	ax-mp	|- ( D ` (/) ) = ( # ` { f | ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) } )
5		ral0	|- A. y e. (/) ( f ` y ) =/= y
6	5	biantru	|- ( f : (/) -1-1-onto-> (/) <-> ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) )
7		eqid	|- (/) = (/)
8		f1o00	|- ( f : (/) -1-1-onto-> (/) <-> ( f = (/) /\ (/) = (/) ) )
9	7 8	mpbiran2	|- ( f : (/) -1-1-onto-> (/) <-> f = (/) )
10	6 9	bitr3i	|- ( ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) <-> f = (/) )
11	10	abbii	|- { f | ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) } = { f | f = (/) }
12		df-sn	|- { (/) } = { f | f = (/) }
13	11 12	eqtr4i	|- { f | ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) } = { (/) }
14	13	fveq2i	|- ( # ` { f | ( f : (/) -1-1-onto-> (/) /\ A. y e. (/) ( f ` y ) =/= y ) } ) = ( # ` { (/) } )
15		0ex	|- (/) e. _V
16		hashsng	|- ( (/) e. _V -> ( # ` { (/) } ) = 1 )
17	15 16	ax-mp	|- ( # ` { (/) } ) = 1
18	4 14 17	3eqtri	|- ( D ` (/) ) = 1