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 = ( SymGrp ` A )
symgov.2
|- B = ( Base ` G )
symgov.3
|- .+ = ( +g ` G )
Assertion symgcl
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )

Proof

Step Hyp Ref Expression
1 symgov.1
 |-  G = ( SymGrp ` A )
2 symgov.2
 |-  B = ( Base ` G )
3 symgov.3
 |-  .+ = ( +g ` G )
4 1 2 3 symgov
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )
5 1 2 symgbasf1o
 |-  ( X e. B -> X : A -1-1-onto-> A )
6 1 2 symgbasf1o
 |-  ( Y e. B -> Y : A -1-1-onto-> A )
7 f1oco
 |-  ( ( X : A -1-1-onto-> A /\ Y : A -1-1-onto-> A ) -> ( X o. Y ) : A -1-1-onto-> A )
8 5 6 7 syl2an
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) : A -1-1-onto-> A )
9 coexg
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )
10 1 2 elsymgbas2
 |-  ( ( X o. Y ) e. _V -> ( ( X o. Y ) e. B <-> ( X o. Y ) : A -1-1-onto-> A ) )
11 9 10 syl
 |-  ( ( X e. B /\ Y e. B ) -> ( ( X o. Y ) e. B <-> ( X o. Y ) : A -1-1-onto-> A ) )
12 8 11 mpbird
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. B )
13 4 12 eqeltrd
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )