Metamath Proof Explorer


Theorem efmndbasfi

Description: The monoid of endofunctions on a finite set A is finite. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndbas.g
|- G = ( EndoFMnd ` A )
efmndbas.b
|- B = ( Base ` G )
Assertion efmndbasfi
|- ( A e. Fin -> B e. Fin )

Proof

Step Hyp Ref Expression
1 efmndbas.g
 |-  G = ( EndoFMnd ` A )
2 efmndbas.b
 |-  B = ( Base ` G )
3 1 2 efmndbas
 |-  B = ( A ^m A )
4 mapfi
 |-  ( ( A e. Fin /\ A e. Fin ) -> ( A ^m A ) e. Fin )
5 4 anidms
 |-  ( A e. Fin -> ( A ^m A ) e. Fin )
6 3 5 eqeltrid
 |-  ( A e. Fin -> B e. Fin )