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