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\in V\to \left\{{\mathrm{I}\upharpoonright }_A\right\}\in \mathrm{SubMnd}\left(G\right)$$

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\in V\to {\mathrm{I}\upharpoonright }_A=0_G$$
3	2	sneqd	$$⊢A\in V\to \left\{{\mathrm{I}\upharpoonright }_A\right\}=\left\{0_G\right\}$$
4	1	efmndmnd	$$⊢A\in V\to G\in \mathrm{Mnd}$$
5		eqid	$$⊢0_G=0_G$$
6	5	0subm	$$⊢G\in \mathrm{Mnd}\to \left\{0_G\right\}\in \mathrm{SubMnd}\left(G\right)$$
7	4 6	syl	$$⊢A\in V\to \left\{0_G\right\}\in \mathrm{SubMnd}\left(G\right)$$
8	3 7	eqeltrd	$$⊢A\in V\to \left\{{\mathrm{I}\upharpoonright }_A\right\}\in \mathrm{SubMnd}\left(G\right)$$