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	syl5eq	⊢ ( 𝐼 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) = 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	syl5eq	⊢ ( 𝐼 ∈ 𝑉 → ( ♯ ‘ 𝐵 ) = 1 )