Metamath Proof Explorer


Theorem symgsubmefmnd

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

Ref Expression
Hypotheses symgsubmefmnd.m No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
symgsubmefmnd.g G=SymGrpA
symgsubmefmnd.b B=BaseG
Assertion symgsubmefmnd AVBSubMndM

Proof

Step Hyp Ref Expression
1 symgsubmefmnd.m Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
2 symgsubmefmnd.g G=SymGrpA
3 symgsubmefmnd.b B=BaseG
4 2 3 symgbas B=f|f:A1-1 ontoA
5 inab f|f:A1-1Af|f:AontoA=f|f:A1-1Af:AontoA
6 df-f1o f:A1-1 ontoAf:A1-1Af:AontoA
7 6 bicomi f:A1-1Af:AontoAf:A1-1 ontoA
8 7 abbii f|f:A1-1Af:AontoA=f|f:A1-1 ontoA
9 5 8 eqtr2i f|f:A1-1 ontoA=f|f:A1-1Af|f:AontoA
10 1 injsubmefmnd AVf|f:A1-1ASubMndM
11 1 sursubmefmnd AVf|f:AontoASubMndM
12 insubm f|f:A1-1ASubMndMf|f:AontoASubMndMf|f:A1-1Af|f:AontoASubMndM
13 10 11 12 syl2anc AVf|f:A1-1Af|f:AontoASubMndM
14 9 13 eqeltrid AVf|f:A1-1 ontoASubMndM
15 4 14 eqeltrid AVBSubMndM