Theorem idressubmefmnd

Description: The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024)

	Ref	Expression
Hypothesis	idressubmefmnd.g	|- G = ( EndoFMnd ` A )
Assertion	idressubmefmnd	|- ( A e. V -> { ( _I |` A ) } e. ( SubMnd ` G ) )

Proof

Step	Hyp	Ref	Expression
1		idressubmefmnd.g	|- G = ( EndoFMnd ` A )
2	1	efmndid	|- ( A e. V -> ( _I |` A ) = ( 0g ` G ) )
3	2	sneqd	|- ( A e. V -> { ( _I |` A ) } = { ( 0g ` G ) } )
4	1	efmndmnd	|- ( A e. V -> G e. Mnd )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	5	0subm	|- ( G e. Mnd -> { ( 0g ` G ) } e. ( SubMnd ` G ) )
7	4 6	syl	|- ( A e. V -> { ( 0g ` G ) } e. ( SubMnd ` G ) )
8	3 7	eqeltrd	|- ( A e. V -> { ( _I |` A ) } e. ( SubMnd ` G ) )