Metamath Proof Explorer


Theorem efmnd1bas

Description: The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024)

Ref Expression
Hypotheses efmnd1bas.1
|- G = ( EndoFMnd ` A )
efmnd1bas.2
|- B = ( Base ` G )
efmnd1bas.0
|- A = { I }
Assertion efmnd1bas
|- ( I e. V -> B = { { <. I , I >. } } )

Proof

Step Hyp Ref Expression
1 efmnd1bas.1
 |-  G = ( EndoFMnd ` A )
2 efmnd1bas.2
 |-  B = ( Base ` G )
3 efmnd1bas.0
 |-  A = { I }
4 3 fveq2i
 |-  ( EndoFMnd ` A ) = ( EndoFMnd ` { I } )
5 1 4 eqtri
 |-  G = ( EndoFMnd ` { I } )
6 5 2 efmndbas
 |-  B = ( { I } ^m { I } )
7 fsng
 |-  ( ( I e. V /\ I e. V ) -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) )
8 7 anidms
 |-  ( I e. V -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) )
9 snex
 |-  { I } e. _V
10 9 9 elmap
 |-  ( p e. ( { I } ^m { I } ) <-> p : { I } --> { I } )
11 velsn
 |-  ( p e. { { <. I , I >. } } <-> p = { <. I , I >. } )
12 8 10 11 3bitr4g
 |-  ( I e. V -> ( p e. ( { I } ^m { I } ) <-> p e. { { <. I , I >. } } ) )
13 12 eqrdv
 |-  ( I e. V -> ( { I } ^m { I } ) = { { <. I , I >. } } )
14 6 13 eqtrid
 |-  ( I e. V -> B = { { <. I , I >. } } )