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 = SymGrp A
symgsubmefmnd.b B = Base G
Assertion symgsubmefmnd A V B SubMnd M

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 = SymGrp A
3 symgsubmefmnd.b B = Base G
4 2 3 symgbas B = f | f : A 1-1 onto A
5 inab f | f : A 1-1 A f | f : A onto A = f | f : A 1-1 A f : A onto A
6 df-f1o f : A 1-1 onto A f : A 1-1 A f : A onto A
7 6 bicomi f : A 1-1 A f : A onto A f : A 1-1 onto A
8 7 abbii f | f : A 1-1 A f : A onto A = f | f : A 1-1 onto A
9 5 8 eqtr2i f | f : A 1-1 onto A = f | f : A 1-1 A f | f : A onto A
10 1 injsubmefmnd A V f | f : A 1-1 A SubMnd M
11 1 sursubmefmnd A V f | f : A onto A SubMnd M
12 insubm f | f : A 1-1 A SubMnd M f | f : A onto A SubMnd M f | f : A 1-1 A f | f : A onto A SubMnd M
13 10 11 12 syl2anc A V f | f : A 1-1 A f | f : A onto A SubMnd M
14 9 13 eqeltrid A V f | f : A 1-1 onto A SubMnd M
15 4 14 eqeltrid A V B SubMnd M