This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )