Theorem symgressbas

Description: The symmetric group on A characterized as structure restriction of the monoid of endofunctions on A to its base set. (Contributed by AV, 30-Mar-2024)

	Ref	Expression
Hypotheses	symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
	symgressbas.m	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
Assertion	symgressbas	⊢ 𝐺 = ( 𝑀 ↾s 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		symgressbas.m	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
4		eqid	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
5	1 4	symgval	⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } )
6	1 2	symgbas	⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
7	3 6	oveq12i	⊢ ( 𝑀 ↾s 𝐵 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } )
8	5 7	eqtr4i	⊢ 𝐺 = ( 𝑀 ↾s 𝐵 )