Theorem deranglem

Description: Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Assertion	deranglem	|- ( A e. Fin -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin )

Proof

Step	Hyp	Ref	Expression
1		mapfi	|- ( ( A e. Fin /\ A e. Fin ) -> ( A ^m A ) e. Fin )
2		f1of	|- ( f : A -1-1-onto-> A -> f : A --> A )
3	2	adantr	|- ( ( f : A -1-1-onto-> A /\ ph ) -> f : A --> A )
4		elmapg	|- ( ( A e. Fin /\ A e. Fin ) -> ( f e. ( A ^m A ) <-> f : A --> A ) )
5	3 4	imbitrrid	|- ( ( A e. Fin /\ A e. Fin ) -> ( ( f : A -1-1-onto-> A /\ ph ) -> f e. ( A ^m A ) ) )
6	5	abssdv	|- ( ( A e. Fin /\ A e. Fin ) -> { f | ( f : A -1-1-onto-> A /\ ph ) } C_ ( A ^m A ) )
7		ssfi	|- ( ( ( A ^m A ) e. Fin /\ { f | ( f : A -1-1-onto-> A /\ ph ) } C_ ( A ^m A ) ) -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin )
8	1 6 7	syl2anc	|- ( ( A e. Fin /\ A e. Fin ) -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin )
9	8	anidms	|- ( A e. Fin -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin )