This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ G = SymGrp (A)$
		symgbas.2	$⊢ B = {Base}_{G}$
		symgressbas.m	$⊢ M = EndoFMnd (A)$
	Assertion	symgressbas	$⊢ G = M ↾_{𝑠} B$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$⊢ G = SymGrp (A)$
2		symgbas.2	$⊢ B = {Base}_{G}$
3		symgressbas.m	$⊢ M = EndoFMnd (A)$
4		eqid	$⊢ \{f \| f : A \underset{1-1 onto}{⟶} A\} = \{f \| f : A \underset{1-1 onto}{⟶} A\}$
5	1 4	symgval	$⊢ G = EndoFMnd (A) ↾_{𝑠} \{f \| f : A \underset{1-1 onto}{⟶} A\}$
6	1 2	symgbas	$⊢ B = \{f \| f : A \underset{1-1 onto}{⟶} A\}$
7	3 6	oveq12i	$⊢ M ↾_{𝑠} B = EndoFMnd (A) ↾_{𝑠} \{f \| f : A \underset{1-1 onto}{⟶} A\}$
8	5 7	eqtr4i	$⊢ G = M ↾_{𝑠} B$