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	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
	symgsubmefmndALT.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgsubmefmndALT.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	symgsubmefmndALT	⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		symgsubmefmndALT.m	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2		symgsubmefmndALT.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
3		symgsubmefmndALT.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4	1	efmndmnd	⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd )
5	2 3 1	symgressbas	⊢ 𝐺 = ( 𝑀 ↾s 𝐵 )
6	2	symggrp	⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )
7		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
8	6 7	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd )
9	5 8	eqeltrrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑀 ↾s 𝐵 ) ∈ Mnd )
10	2	idresperm	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )
11	1	efmndid	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝑀 ) )
12	3	eqcomi	⊢ ( Base ‘ 𝐺 ) = 𝐵
13	12	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐺 ) = 𝐵 )
14	10 11 13	3eltr3d	⊢ ( 𝐴 ∈ 𝑉 → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
15	2 3	symgbasmap	⊢ ( 𝑓 ∈ 𝐵 → 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) )
16	15	ssriv	⊢ 𝐵 ⊆ ( 𝐴 ↑m 𝐴 )
17		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
18	1 17	efmndbas	⊢ ( Base ‘ 𝑀 ) = ( 𝐴 ↑m 𝐴 )
19	16 18	sseqtrri	⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
20	14 19	jctil	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) )
21		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
22	17 21	issubmndb	⊢ ( 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 𝑀 ∈ Mnd ∧ ( 𝑀 ↾s 𝐵 ) ∈ Mnd ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) ) )
23	4 9 20 22	syl21anbrc	⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )