This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )