Metamath Proof Explorer


Theorem efmnd1hash

Description: The monoid of endofunctions on a singleton has cardinality 1 . (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmnd1bas.1 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmnd1bas.2 𝐵 = ( Base ‘ 𝐺 )
efmnd1bas.0 𝐴 = { 𝐼 }
Assertion efmnd1hash ( 𝐼𝑉 → ( ♯ ‘ 𝐵 ) = 1 )

Proof

Step Hyp Ref Expression
1 efmnd1bas.1 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmnd1bas.2 𝐵 = ( Base ‘ 𝐺 )
3 efmnd1bas.0 𝐴 = { 𝐼 }
4 snfi { 𝐼 } ∈ Fin
5 3 4 eqeltri 𝐴 ∈ Fin
6 1 2 efmndhash ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) )
7 5 6 ax-mp ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) )
8 3 fveq2i ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝐼 } )
9 hashsng ( 𝐼𝑉 → ( ♯ ‘ { 𝐼 } ) = 1 )
10 8 9 eqtrid ( 𝐼𝑉 → ( ♯ ‘ 𝐴 ) = 1 )
11 10 10 oveq12d ( 𝐼𝑉 → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) = ( 1 ↑ 1 ) )
12 1z 1 ∈ ℤ
13 1exp ( 1 ∈ ℤ → ( 1 ↑ 1 ) = 1 )
14 12 13 ax-mp ( 1 ↑ 1 ) = 1
15 11 14 eqtrdi ( 𝐼𝑉 → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) = 1 )
16 7 15 eqtrid ( 𝐼𝑉 → ( ♯ ‘ 𝐵 ) = 1 )