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 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion efmndhash ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 efmndbas 𝐵 = ( 𝐴m 𝐴 )
4 3 a1i ( 𝐴 ∈ Fin → 𝐵 = ( 𝐴m 𝐴 ) )
5 4 fveq2d ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 𝐴m 𝐴 ) ) )
6 hashmap ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ ( 𝐴m 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) )
7 6 anidms ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴m 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) )
8 5 7 eqtrd ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) )