Metamath Proof Explorer


Theorem injsubmefmnd

Description: The set of injective endofunctions on a set A is a submonoid of the monoid of endofunctions on A . (Contributed by AV, 25-Feb-2024)

Ref Expression
Hypothesis sursubmefmnd.m No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
Assertion injsubmefmnd AVh|h:A1-1ASubMndM

Proof

Step Hyp Ref Expression
1 sursubmefmnd.m Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
2 vex xV
3 f1eq1 h=xh:A1-1Ax:A1-1A
4 2 3 elab xh|h:A1-1Ax:A1-1A
5 f1f x:A1-1Ax:AA
6 eqid BaseM=BaseM
7 1 6 elefmndbas AVxBaseMx:AA
8 5 7 syl5ibr AVx:A1-1AxBaseM
9 4 8 syl5bi AVxh|h:A1-1AxBaseM
10 9 ssrdv AVh|h:A1-1ABaseM
11 1 efmndid AVIA=0M
12 resiexg AVIAV
13 f1oi IA:A1-1 ontoA
14 f1of1 IA:A1-1 ontoAIA:A1-1A
15 13 14 mp1i AVIA:A1-1A
16 f1eq1 h=IAh:A1-1AIA:A1-1A
17 12 15 16 elabd AVIAh|h:A1-1A
18 11 17 eqeltrrd AV0Mh|h:A1-1A
19 vex yV
20 f1eq1 h=yh:A1-1Ay:A1-1A
21 19 20 elab yh|h:A1-1Ay:A1-1A
22 4 21 anbi12i xh|h:A1-1Ayh|h:A1-1Ax:A1-1Ay:A1-1A
23 f1co x:A1-1Ay:A1-1Axy:A1-1A
24 23 adantl AVx:A1-1Ay:A1-1Axy:A1-1A
25 f1f y:A1-1Ay:AA
26 5 25 anim12i x:A1-1Ay:A1-1Ax:AAy:AA
27 1 6 elefmndbas AVyBaseMy:AA
28 7 27 anbi12d AVxBaseMyBaseMx:AAy:AA
29 26 28 syl5ibr AVx:A1-1Ay:A1-1AxBaseMyBaseM
30 29 imp AVx:A1-1Ay:A1-1AxBaseMyBaseM
31 eqid +M=+M
32 1 6 31 efmndov xBaseMyBaseMx+My=xy
33 30 32 syl AVx:A1-1Ay:A1-1Ax+My=xy
34 33 eleq1d AVx:A1-1Ay:A1-1Ax+Myh|h:A1-1Axyh|h:A1-1A
35 2 19 coex xyV
36 f1eq1 h=xyh:A1-1Axy:A1-1A
37 35 36 elab xyh|h:A1-1Axy:A1-1A
38 34 37 bitrdi AVx:A1-1Ay:A1-1Ax+Myh|h:A1-1Axy:A1-1A
39 24 38 mpbird AVx:A1-1Ay:A1-1Ax+Myh|h:A1-1A
40 39 ex AVx:A1-1Ay:A1-1Ax+Myh|h:A1-1A
41 22 40 syl5bi AVxh|h:A1-1Ayh|h:A1-1Ax+Myh|h:A1-1A
42 41 ralrimivv AVxh|h:A1-1Ayh|h:A1-1Ax+Myh|h:A1-1A
43 1 efmndmnd AVMMnd
44 eqid 0M=0M
45 6 44 31 issubm MMndh|h:A1-1ASubMndMh|h:A1-1ABaseM0Mh|h:A1-1Axh|h:A1-1Ayh|h:A1-1Ax+Myh|h:A1-1A
46 43 45 syl AVh|h:A1-1ASubMndMh|h:A1-1ABaseM0Mh|h:A1-1Axh|h:A1-1Ayh|h:A1-1Ax+Myh|h:A1-1A
47 10 18 42 46 mpbir3and AVh|h:A1-1ASubMndM