Metamath Proof Explorer


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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
efmndbas.b B = Base G
Assertion efmndhash A Fin B = A A

Proof

Step Hyp Ref Expression
1 efmndbas.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 efmndbas.b B = Base G
3 1 2 efmndbas B = A A
4 3 a1i A Fin B = A A
5 4 fveq2d A Fin B = A A
6 hashmap A Fin A Fin A A = A A
7 6 anidms A Fin A A = A A
8 5 7 eqtrd A Fin B = A A