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=BaseG
efmnd1bas.0 A=I
Assertion efmnd1hash IVB=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=BaseG
3 efmnd1bas.0 A=I
4 snfi IFin
5 3 4 eqeltri AFin
6 1 2 efmndhash AFinB=AA
7 5 6 ax-mp B=AA
8 3 fveq2i A=I
9 hashsng IVI=1
10 8 9 eqtrid IVA=1
11 10 10 oveq12d IVAA=11
12 1z 1
13 1exp 111=1
14 12 13 ax-mp 11=1
15 11 14 eqtrdi IVAA=1
16 7 15 eqtrid IVB=1