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 | |
||
symgsubmefmnd.b | |
||
Assertion | symgsubmefmnd | |
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 | |
|
3 | symgsubmefmnd.b | |
|
4 | 2 3 | symgbas | |
5 | inab | |
|
6 | df-f1o | |
|
7 | 6 | bicomi | |
8 | 7 | abbii | |
9 | 5 8 | eqtr2i | |
10 | 1 | injsubmefmnd | |
11 | 1 | sursubmefmnd | |
12 | insubm | |
|
13 | 10 11 12 | syl2anc | |
14 | 9 13 | eqeltrid | |
15 | 4 14 | eqeltrid | |