Metamath Proof Explorer


Theorem ielefmnd

Description: The identity function restricted to a set A is an element of the base set of the monoid of endofunctions on A . (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypothesis ielefmnd.g
|- G = ( EndoFMnd ` A )
Assertion ielefmnd
|- ( A e. V -> ( _I |` A ) e. ( Base ` G ) )

Proof

Step Hyp Ref Expression
1 ielefmnd.g
 |-  G = ( EndoFMnd ` A )
2 f1oi
 |-  ( _I |` A ) : A -1-1-onto-> A
3 f1of
 |-  ( ( _I |` A ) : A -1-1-onto-> A -> ( _I |` A ) : A --> A )
4 2 3 ax-mp
 |-  ( _I |` A ) : A --> A
5 eqid
 |-  ( Base ` G ) = ( Base ` G )
6 1 5 elefmndbas
 |-  ( A e. V -> ( ( _I |` A ) e. ( Base ` G ) <-> ( _I |` A ) : A --> A ) )
7 4 6 mpbiri
 |-  ( A e. V -> ( _I |` A ) e. ( Base ` G ) )