This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )