Theorem efmnd1hash

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

	Ref	Expression
Hypotheses	efmnd1bas.1	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmnd1bas.2	$$⊢B={\mathrm{Base}}_G$$
	efmnd1bas.0	$$⊢A=\left\{I\right\}$$
Assertion	efmnd1hash	$$⊢I\in V\to \left|B\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		efmnd1bas.1	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		efmnd1bas.2	$$⊢B={\mathrm{Base}}_G$$
3		efmnd1bas.0	$$⊢A=\left\{I\right\}$$
4		snfi	$$⊢\left\{I\right\}\in \mathrm{Fin}$$
5	3 4	eqeltri	$$⊢A\in \mathrm{Fin}$$
6	1 2	efmndhash	$$⊢A\in \mathrm{Fin}\to \left|B\right|={\left|A\right|}^{\left|A\right|}$$
7	5 6	ax-mp	$$⊢\left|B\right|={\left|A\right|}^{\left|A\right|}$$
8	3	fveq2i	$$⊢\left|A\right|=\left|\left\{I\right\}\right|$$
9		hashsng	$$⊢I\in V\to \left|\left\{I\right\}\right|=1$$
10	8 9	syl5eq	$$⊢I\in V\to \left|A\right|=1$$
11	10 10	oveq12d	$$⊢I\in V\to {\left|A\right|}^{\left|A\right|}=1^1$$
12		1z	$$⊢1\in \mathbb{Z}$$
13		1exp	$$⊢1\in \mathbb{Z}\to 1^1=1$$
14	12 13	ax-mp	$$⊢1^1=1$$
15	11 14	eqtrdi	$$⊢I\in V\to {\left|A\right|}^{\left|A\right|}=1$$
16	7 15	syl5eq	$$⊢I\in V\to \left|B\right|=1$$