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 → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) ) |
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 → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) ) |