Theorem symgcl

Description: The group operation of the symmetric group on A is closed, i.e. a magma. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by Mario Carneiro, 28-Jan-2015)

	Ref	Expression
Hypotheses	symgov.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgov.2	$$⊢B={\mathrm{Base}}_G$$
	symgov.3	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	symgcl	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		symgov.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgov.2	$$⊢B={\mathrm{Base}}_G$$
3		symgov.3	$$⊢\underset{\dot{}}{+}={+}_G$$
4	1 2 3	symgov	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$
5	1 2	symgbasf1o	$$⊢X\in B\to X:A\underset{1-1\; onto}{⟶}A$$
6	1 2	symgbasf1o	$$⊢Y\in B\to Y:A\underset{1-1\; onto}{⟶}A$$
7		f1oco	$$⊢\left(X:A\underset{1-1\; onto}{⟶}A\wedge Y:A\underset{1-1\; onto}{⟶}A\right)\to \left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A$$
8	5 6 7	syl2an	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A$$
9		coexg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in \mathrm{V}$$
10	1 2	elsymgbas2	$$⊢X\circ Y\in \mathrm{V}\to \left(X\circ Y\in B\leftrightarrow \left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A\right)$$
11	9 10	syl	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\circ Y\in B\leftrightarrow \left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A\right)$$
12	8 11	mpbird	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in B$$
13	4 12	eqeltrd	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$