Theorem efmnd1hash

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

	Ref	Expression
Hypotheses	efmnd1bas.1	|- G = ( EndoFMnd ` A )
	efmnd1bas.2	|- B = ( Base ` G )
	efmnd1bas.0	|- A = { I }
Assertion	efmnd1hash	|- ( I e. V -> ( # ` B ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		efmnd1bas.1	|- G = ( EndoFMnd ` A )
2		efmnd1bas.2	|- B = ( Base ` G )
3		efmnd1bas.0	|- A = { I }
4		snfi	|- { I } e. Fin
5	3 4	eqeltri	|- A e. Fin
6	1 2	efmndhash	|- ( A e. Fin -> ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) ) )
7	5 6	ax-mp	|- ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) )
8	3	fveq2i	|- ( # ` A ) = ( # ` { I } )
9		hashsng	|- ( I e. V -> ( # ` { I } ) = 1 )
10	8 9	eqtrid	|- ( I e. V -> ( # ` A ) = 1 )
11	10 10	oveq12d	|- ( I e. V -> ( ( # ` A ) ^ ( # ` A ) ) = ( 1 ^ 1 ) )
12		1z	|- 1 e. ZZ
13		1exp	|- ( 1 e. ZZ -> ( 1 ^ 1 ) = 1 )
14	12 13	ax-mp	|- ( 1 ^ 1 ) = 1
15	11 14	eqtrdi	|- ( I e. V -> ( ( # ` A ) ^ ( # ` A ) ) = 1 )
16	7 15	eqtrid	|- ( I e. V -> ( # ` B ) = 1 )