Metamath Proof Explorer


Theorem idresefmnd

Description: The structure with the singleton containing only the identity function restricted to a set A as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on A to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on A . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses idressubmefmnd.g No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
idresefmnd.e E=G𝑠IA
Assertion idresefmnd AVEMndBaseEBaseG

Proof

Step Hyp Ref Expression
1 idressubmefmnd.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 idresefmnd.e E=G𝑠IA
3 1 idressubmefmnd AVIASubMndG
4 1 efmndmnd AVGMnd
5 eqid BaseG=BaseG
6 eqid 0G=0G
7 eqid G𝑠IA=G𝑠IA
8 5 6 7 issubm2 GMndIASubMndGIABaseG0GIAG𝑠IAMnd
9 4 8 syl AVIASubMndGIABaseG0GIAG𝑠IAMnd
10 snex IAV
11 2 5 ressbas IAVIABaseG=BaseE
12 10 11 mp1i AVIABaseG=BaseE
13 inss2 IABaseGBaseG
14 12 13 eqsstrrdi AVBaseEBaseG
15 2 eqcomi G𝑠IA=E
16 15 eleq1i G𝑠IAMndEMnd
17 16 biimpi G𝑠IAMndEMnd
18 17 3ad2ant3 IABaseG0GIAG𝑠IAMndEMnd
19 14 18 anim12ci AVIABaseG0GIAG𝑠IAMndEMndBaseEBaseG
20 19 ex AVIABaseG0GIAG𝑠IAMndEMndBaseEBaseG
21 9 20 sylbid AVIASubMndGEMndBaseEBaseG
22 3 21 mpd AVEMndBaseEBaseG