Theorem symgsubmefmndALT

Description: The symmetric group on a set A is a submonoid of the monoid of endofunctions on A . Alternate proof based on issubmndb and not on injsubmefmnd and sursubmefmnd . (Contributed by AV, 18-Feb-2024) (Revised by AV, 30-Mar-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	symgsubmefmndALT.m	|- M = ( EndoFMnd ` A )
	symgsubmefmndALT.g	|- G = ( SymGrp ` A )
	symgsubmefmndALT.b	|- B = ( Base ` G )
Assertion	symgsubmefmndALT	|- ( A e. V -> B e. ( SubMnd ` M ) )

Proof

Step	Hyp	Ref	Expression
1		symgsubmefmndALT.m	|- M = ( EndoFMnd ` A )
2		symgsubmefmndALT.g	|- G = ( SymGrp ` A )
3		symgsubmefmndALT.b	|- B = ( Base ` G )
4	1	efmndmnd	|- ( A e. V -> M e. Mnd )
5	2 3 1	symgressbas	|- G = ( M |`s B )
6	2	symggrp	|- ( A e. V -> G e. Grp )
7		grpmnd	|- ( G e. Grp -> G e. Mnd )
8	6 7	syl	|- ( A e. V -> G e. Mnd )
9	5 8	eqeltrrid	|- ( A e. V -> ( M |`s B ) e. Mnd )
10	2	idresperm	|- ( A e. V -> ( _I |` A ) e. ( Base ` G ) )
11	1	efmndid	|- ( A e. V -> ( _I |` A ) = ( 0g ` M ) )
12	3	eqcomi	|- ( Base ` G ) = B
13	12	a1i	|- ( A e. V -> ( Base ` G ) = B )
14	10 11 13	3eltr3d	|- ( A e. V -> ( 0g ` M ) e. B )
15	2 3	symgbasmap	|- ( f e. B -> f e. ( A ^m A ) )
16	15	ssriv	|- B C_ ( A ^m A )
17		eqid	|- ( Base ` M ) = ( Base ` M )
18	1 17	efmndbas	|- ( Base ` M ) = ( A ^m A )
19	16 18	sseqtrri	|- B C_ ( Base ` M )
20	14 19	jctil	|- ( A e. V -> ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B ) )
21		eqid	|- ( 0g ` M ) = ( 0g ` M )
22	17 21	issubmndb	|- ( B e. ( SubMnd ` M ) <-> ( ( M e. Mnd /\ ( M |`s B ) e. Mnd ) /\ ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B ) ) )
23	4 9 20 22	syl21anbrc	|- ( A e. V -> B e. ( SubMnd ` M ) )