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
|- 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 )