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