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 𝑠 I A
Assertion idresefmnd A V E Mnd Base E Base 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 idresefmnd.e E = G 𝑠 I A
3 1 idressubmefmnd A V I A SubMnd G
4 1 efmndmnd A V G Mnd
5 eqid Base G = Base G
6 eqid 0 G = 0 G
7 eqid G 𝑠 I A = G 𝑠 I A
8 5 6 7 issubm2 G Mnd I A SubMnd G I A Base G 0 G I A G 𝑠 I A Mnd
9 4 8 syl A V I A SubMnd G I A Base G 0 G I A G 𝑠 I A Mnd
10 snex I A V
11 2 5 ressbas I A V I A Base G = Base E
12 10 11 mp1i A V I A Base G = Base E
13 inss2 I A Base G Base G
14 12 13 eqsstrrdi A V Base E Base G
15 2 eqcomi G 𝑠 I A = E
16 15 eleq1i G 𝑠 I A Mnd E Mnd
17 16 biimpi G 𝑠 I A Mnd E Mnd
18 17 3ad2ant3 I A Base G 0 G I A G 𝑠 I A Mnd E Mnd
19 14 18 anim12ci A V I A Base G 0 G I A G 𝑠 I A Mnd E Mnd Base E Base G
20 19 ex A V I A Base G 0 G I A G 𝑠 I A Mnd E Mnd Base E Base G
21 9 20 sylbid A V I A SubMnd G E Mnd Base E Base G
22 3 21 mpd A V E Mnd Base E Base G