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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion idressubmefmnd A V I A SubMnd G

Proof

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 A V I A = 0 G
3 2 sneqd A V I A = 0 G
4 1 efmndmnd A V G Mnd
5 eqid 0 G = 0 G
6 5 0subm G Mnd 0 G SubMnd G
7 4 6 syl A V 0 G SubMnd G
8 3 7 eqeltrd A V I A SubMnd G