Theorem derangen

Description: The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-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	derangen	|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` A ) = ( D ` B ) )

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	1	derangenlem	|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` A ) <_ ( D ` B ) )
3		ensym	|- ( A ~~ B -> B ~~ A )
4	3	adantr	|- ( ( A ~~ B /\ B e. Fin ) -> B ~~ A )
5		enfi	|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )
6	5	biimpar	|- ( ( A ~~ B /\ B e. Fin ) -> A e. Fin )
7	1	derangenlem	|- ( ( B ~~ A /\ A e. Fin ) -> ( D ` B ) <_ ( D ` A ) )
8	4 6 7	syl2anc	|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` B ) <_ ( D ` A ) )
9	1	derangf	|- D : Fin --> NN0
10	9	ffvelrni	|- ( A e. Fin -> ( D ` A ) e. NN0 )
11	6 10	syl	|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` A ) e. NN0 )
12	9	ffvelrni	|- ( B e. Fin -> ( D ` B ) e. NN0 )
13	12	adantl	|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` B ) e. NN0 )
14		nn0re	|- ( ( D ` A ) e. NN0 -> ( D ` A ) e. RR )
15		nn0re	|- ( ( D ` B ) e. NN0 -> ( D ` B ) e. RR )
16		letri3	|- ( ( ( D ` A ) e. RR /\ ( D ` B ) e. RR ) -> ( ( D ` A ) = ( D ` B ) <-> ( ( D ` A ) <_ ( D ` B ) /\ ( D ` B ) <_ ( D ` A ) ) ) )
17	14 15 16	syl2an	|- ( ( ( D ` A ) e. NN0 /\ ( D ` B ) e. NN0 ) -> ( ( D ` A ) = ( D ` B ) <-> ( ( D ` A ) <_ ( D ` B ) /\ ( D ` B ) <_ ( D ` A ) ) ) )
18	11 13 17	syl2anc	|- ( ( A ~~ B /\ B e. Fin ) -> ( ( D ` A ) = ( D ` B ) <-> ( ( D ` A ) <_ ( D ` B ) /\ ( D ` B ) <_ ( D ` A ) ) ) )
19	2 8 18	mpbir2and	|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` A ) = ( D ` B ) )