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 | No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |- | |
Assertion | idressubmefmnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idressubmefmnd.g | Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |- | |
2 | 1 | efmndid | |
3 | 2 | sneqd | |
4 | 1 | efmndmnd | |
5 | eqid | ||
6 | 5 | 0subm | |
7 | 4 6 | syl | |
8 | 3 7 | eqeltrd |