Metamath Proof Explorer


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 syl5ibr
 |-  ( ( 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 )