Theorem symgbas

Description: The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015) (Proof shortened by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbas	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3		eqid	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
4	1 3	symgval	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
5	4	eqcomi	$$⊢\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}=G$$
6	5	fveq2i	$$⊢{\mathrm{Base}}_{\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\right)}={\mathrm{Base}}_G$$
7		f1of	$$⊢x:A\underset{1-1\; onto}{⟶}A\to x:A⟶A$$
8	7	ss2abi	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\subseteq \left\{x|x:A⟶A\right\}$$
9		eqid	$$⊢\mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(A\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
11	9 10	efmndbasabf	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}=\left\{x|x:A⟶A\right\}$$
12	8 11	sseqtrri	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\subseteq {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
13		eqid	$$⊢\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
14	13 10	ressbas2	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\subseteq {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}\to \left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}={\mathrm{Base}}_{\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\right)}$$
15	12 14	ax-mp	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}={\mathrm{Base}}_{\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\right)}$$
16	6 15 2	3eqtr4ri	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$