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

Proof

Step	Hyp	Ref	Expression
1		symgsubmefmnd.m	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2		symgsubmefmnd.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
3		symgsubmefmnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4	2 3	symgbas	⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
5		inab	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ) = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) }
6		df-f1o	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ↔ ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) )
7	6	bicomi	⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐴 )
8	7	abbii	⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
9	5 8	eqtr2i	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } = ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } )
10	1	injsubmefmnd	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )
11	1	sursubmefmnd	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )
12		insubm	⊢ ( ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) ∧ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) ) → ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ) ∈ ( SubMnd ‘ 𝑀 ) )
13	10 11 12	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ) ∈ ( SubMnd ‘ 𝑀 ) )
14	9 13	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )
15	4 14	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )