# Metamath Proof Explorer

## 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
Assertion symgcl

### Proof

Step Hyp Ref Expression
1 symgov.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 symgov.2 ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 symgov.3
4 1 2 3 symgov
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}↔\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}↔\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