Theorem efmndhash

Description: The monoid of endofunctions on n objects has cardinality n ^ n . (Contributed by AV, 27-Jan-2024)

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

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	3	a1i	|- ( A e. Fin -> B = ( A ^m A ) )
5	4	fveq2d	|- ( A e. Fin -> ( # ` B ) = ( # ` ( A ^m A ) ) )
6		hashmap	|- ( ( A e. Fin /\ A e. Fin ) -> ( # ` ( A ^m A ) ) = ( ( # ` A ) ^ ( # ` A ) ) )
7	6	anidms	|- ( A e. Fin -> ( # ` ( A ^m A ) ) = ( ( # ` A ) ^ ( # ` A ) ) )
8	5 7	eqtrd	|- ( A e. Fin -> ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) ) )