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