Theorem symggrp

Description: The symmetric group on a set A is a group. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 28-Jan-2024)

	Ref	Expression
Hypothesis	symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
Assertion	symggrp	$$⊢A\in V\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		eqidd	$$⊢A\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqidd	$$⊢A\in V\to {+}_G={+}_G$$
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5		eqid	$$⊢{+}_G={+}_G$$
6	1 4 5	symgcl	$$⊢\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\to x{+}_{G}y\in {\mathrm{Base}}_G$$
7	6	3adant1	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\to x{+}_{G}y\in {\mathrm{Base}}_G$$
8	1 4 5	symgcl	$$⊢\left(f\in {\mathrm{Base}}_G\wedge g\in {\mathrm{Base}}_G\right)\to f{+}_{G}g\in {\mathrm{Base}}_G$$
9	1 4 5	symgov	$$⊢\left(f\in {\mathrm{Base}}_G\wedge g\in {\mathrm{Base}}_G\right)\to f{+}_{G}g=f\circ g$$
10	8 9	symggrplem	$$⊢\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\wedge z\in {\mathrm{Base}}_G\right)\to \left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)$$
11	10	adantl	$$⊢\left(A\in V\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\wedge z\in {\mathrm{Base}}_G\right)\right)\to \left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)$$
12	1	idresperm	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G$$
13	1 4 5	symgov	$$⊢\left({\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G\wedge x\in {\mathrm{Base}}_G\right)\to \left({\mathrm{I}\upharpoonright }_A\right){+}_{G}x=\left({\mathrm{I}\upharpoonright }_A\right)\circ x$$
14	12 13	sylan	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to \left({\mathrm{I}\upharpoonright }_A\right){+}_{G}x=\left({\mathrm{I}\upharpoonright }_A\right)\circ x$$
15	1 4	elsymgbas	$$⊢A\in V\to \left(x\in {\mathrm{Base}}_G\leftrightarrow x:A\underset{1-1\; onto}{⟶}A\right)$$
16	15	biimpa	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to x:A\underset{1-1\; onto}{⟶}A$$
17		f1of	$$⊢x:A\underset{1-1\; onto}{⟶}A\to x:A⟶A$$
18		fcoi2	$$⊢x:A⟶A\to \left({\mathrm{I}\upharpoonright }_A\right)\circ x=x$$
19	16 17 18	3syl	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to \left({\mathrm{I}\upharpoonright }_A\right)\circ x=x$$
20	14 19	eqtrd	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to \left({\mathrm{I}\upharpoonright }_A\right){+}_{G}x=x$$
21		f1ocnv	$$⊢x:A\underset{1-1\; onto}{⟶}A\to x^{-1}:A\underset{1-1\; onto}{⟶}A$$
22	21	a1i	$$⊢A\in V\to \left(x:A\underset{1-1\; onto}{⟶}A\to x^{-1}:A\underset{1-1\; onto}{⟶}A\right)$$
23	1 4	elsymgbas	$$⊢A\in V\to \left(x^{-1}\in {\mathrm{Base}}_G\leftrightarrow x^{-1}:A\underset{1-1\; onto}{⟶}A\right)$$
24	22 15 23	3imtr4d	$$⊢A\in V\to \left(x\in {\mathrm{Base}}_G\to x^{-1}\in {\mathrm{Base}}_G\right)$$
25	24	imp	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to x^{-1}\in {\mathrm{Base}}_G$$
26	1 4 5	symgov	$$⊢\left(x^{-1}\in {\mathrm{Base}}_G\wedge x\in {\mathrm{Base}}_G\right)\to x^{-1}{+}_{G}x=x^{-1}\circ x$$
27	25 26	sylancom	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to x^{-1}{+}_{G}x=x^{-1}\circ x$$
28		f1ococnv1	$$⊢x:A\underset{1-1\; onto}{⟶}A\to x^{-1}\circ x={\mathrm{I}\upharpoonright }_A$$
29	16 28	syl	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to x^{-1}\circ x={\mathrm{I}\upharpoonright }_A$$
30	27 29	eqtrd	$$⊢\left(A\in V\wedge x\in {\mathrm{Base}}_G\right)\to x^{-1}{+}_{G}x={\mathrm{I}\upharpoonright }_A$$
31	2 3 7 11 12 20 25 30	isgrpd	$$⊢A\in V\to G\in \mathrm{Grp}$$