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	|- M = ( EndoFMnd ` A )
	symgsubmefmnd.g	|- G = ( SymGrp ` A )
	symgsubmefmnd.b	|- B = ( Base ` G )
Assertion	symgsubmefmnd	|- ( A e. V -> B e. ( SubMnd ` M ) )

Proof

Step	Hyp	Ref	Expression
1		symgsubmefmnd.m	|- M = ( EndoFMnd ` A )
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 } i^i { 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 } i^i { f | f : A -onto-> A } )
10	1	injsubmefmnd	|- ( A e. V -> { f | f : A -1-1-> A } e. ( SubMnd ` M ) )
11	1	sursubmefmnd	|- ( A e. V -> { f | f : A -onto-> A } e. ( SubMnd ` M ) )
12		insubm	|- ( ( { f | f : A -1-1-> A } e. ( SubMnd ` M ) /\ { f | f : A -onto-> A } e. ( SubMnd ` M ) ) -> ( { f | f : A -1-1-> A } i^i { f | f : A -onto-> A } ) e. ( SubMnd ` M ) )
13	10 11 12	syl2anc	|- ( A e. V -> ( { f | f : A -1-1-> A } i^i { f | f : A -onto-> A } ) e. ( SubMnd ` M ) )
14	9 13	eqeltrid	|- ( A e. V -> { f | f : A -1-1-onto-> A } e. ( SubMnd ` M ) )
15	4 14	eqeltrid	|- ( A e. V -> B e. ( SubMnd ` M ) )