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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
efmnd1bas.2 B = Base G
efmnd1bas.0 A = I
Assertion efmnd1hash I V B = 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 = Base G
3 efmnd1bas.0 A = I
4 snfi I Fin
5 3 4 eqeltri A Fin
6 1 2 efmndhash A Fin B = A A
7 5 6 ax-mp B = A A
8 3 fveq2i A = I
9 hashsng I V I = 1
10 8 9 eqtrid I V A = 1
11 10 10 oveq12d I V A A = 1 1
12 1z 1
13 1exp 1 1 1 = 1
14 12 13 ax-mp 1 1 = 1
15 11 14 eqtrdi I V A A = 1
16 7 15 eqtrid I V B = 1