Metamath Proof Explorer


Theorem sursubmefmnd

Description: The set of surjective 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 sursubmefmnd AVh|h:AontoASubMndM

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 foeq1 h=xh:AontoAx:AontoA
4 2 3 elab xh|h:AontoAx:AontoA
5 fof x:AontoAx:AA
6 eqid BaseM=BaseM
7 1 6 elefmndbas AVxBaseMx:AA
8 5 7 syl5ibr AVx:AontoAxBaseM
9 4 8 syl5bi AVxh|h:AontoAxBaseM
10 9 ssrdv AVh|h:AontoABaseM
11 1 efmndid AVIA=0M
12 resiexg AVIAV
13 f1oi IA:A1-1 ontoA
14 f1ofo IA:A1-1 ontoAIA:AontoA
15 13 14 mp1i AVIA:AontoA
16 foeq1 h=IAh:AontoAIA:AontoA
17 12 15 16 elabd AVIAh|h:AontoA
18 11 17 eqeltrrd AV0Mh|h:AontoA
19 vex yV
20 foeq1 h=yh:AontoAy:AontoA
21 19 20 elab yh|h:AontoAy:AontoA
22 4 21 anbi12i xh|h:AontoAyh|h:AontoAx:AontoAy:AontoA
23 foco x:AontoAy:AontoAxy:AontoA
24 23 adantl AVx:AontoAy:AontoAxy:AontoA
25 fof y:AontoAy:AA
26 5 25 anim12i x:AontoAy:AontoAx:AAy:AA
27 1 6 elefmndbas AVyBaseMy:AA
28 7 27 anbi12d AVxBaseMyBaseMx:AAy:AA
29 26 28 syl5ibr AVx:AontoAy:AontoAxBaseMyBaseM
30 29 imp AVx:AontoAy:AontoAxBaseMyBaseM
31 eqid +M=+M
32 1 6 31 efmndov xBaseMyBaseMx+My=xy
33 30 32 syl AVx:AontoAy:AontoAx+My=xy
34 33 eleq1d AVx:AontoAy:AontoAx+Myh|h:AontoAxyh|h:AontoA
35 2 19 coex xyV
36 foeq1 h=xyh:AontoAxy:AontoA
37 35 36 elab xyh|h:AontoAxy:AontoA
38 34 37 bitrdi AVx:AontoAy:AontoAx+Myh|h:AontoAxy:AontoA
39 24 38 mpbird AVx:AontoAy:AontoAx+Myh|h:AontoA
40 39 ex AVx:AontoAy:AontoAx+Myh|h:AontoA
41 22 40 syl5bi AVxh|h:AontoAyh|h:AontoAx+Myh|h:AontoA
42 41 ralrimivv AVxh|h:AontoAyh|h:AontoAx+Myh|h:AontoA
43 1 efmndmnd AVMMnd
44 eqid 0M=0M
45 6 44 31 issubm MMndh|h:AontoASubMndMh|h:AontoABaseM0Mh|h:AontoAxh|h:AontoAyh|h:AontoAx+Myh|h:AontoA
46 43 45 syl AVh|h:AontoASubMndMh|h:AontoABaseM0Mh|h:AontoAxh|h:AontoAyh|h:AontoAx+Myh|h:AontoA
47 10 18 42 46 mpbir3and AVh|h:AontoASubMndM