Metamath Proof Explorer


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