# Metamath Proof Explorer

## Theorem symgplusg

Description: The group operation of a symmetric group is the function composition. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015) (Proof shortened by AV, 19-Feb-2024) (Revised by AV, 29-Mar-2024)

Ref Expression
Hypotheses symgplusg.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
symgplusg.2 ${⊢}{B}={{A}}^{{A}}$
symgplusg.3
Assertion symgplusg

### Proof

Step Hyp Ref Expression
1 symgplusg.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 symgplusg.2 ${⊢}{B}={{A}}^{{A}}$
3 symgplusg.3
4 permsetex ${⊢}{A}\in \mathrm{V}\to \left\{{f}|{f}:{A}\underset{1-1 onto}{⟶}{A}\right\}\in \mathrm{V}$
5 eqid Could not format ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) with typecode |-
6 eqid Could not format ( +g  ( EndoFMnd  A ) ) = ( +g  ( EndoFMnd  A ) ) : No typesetting found for |- ( +g  ( EndoFMnd  A ) ) = ( +g  ( EndoFMnd  A ) ) with typecode |-
7 5 6 ressplusg Could not format ( { f | f : A -1-1-onto-> A } e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( { f | f : A -1-1-onto-> A } e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) ) ) with typecode |-
8 4 7 syl Could not format ( A e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( A e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) ) ) with typecode |-
9 eqid ${⊢}\left\{{f}|{f}:{A}\underset{1-1 onto}{⟶}{A}\right\}=\left\{{f}|{f}:{A}\underset{1-1 onto}{⟶}{A}\right\}$
10 1 9 symgval Could not format G = ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- G = ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) with typecode |-
11 10 eqcomi Could not format ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) = G : No typesetting found for |- ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) = G with typecode |-
12 11 fveq2i Could not format ( +g  ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) ) = ( +g  G ) : No typesetting found for |- ( +g  ( ( EndoFMnd  A ) |s { f | f : A -1-1-onto-> A } ) ) = ( +g  G ) with typecode |-
13 8 12 eqtrdi Could not format ( A e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  G ) ) : No typesetting found for |- ( A e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  G ) ) with typecode |-
14 fvprc Could not format ( -. A e. _V -> ( EndoFMnd  A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd  A ) = (/) ) with typecode |-
15 fvprc ${⊢}¬{A}\in \mathrm{V}\to \mathrm{SymGrp}\left({A}\right)=\varnothing$
16 1 15 syl5req ${⊢}¬{A}\in \mathrm{V}\to \varnothing ={G}$
17 14 16 eqtrd Could not format ( -. A e. _V -> ( EndoFMnd  A ) = G ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd  A ) = G ) with typecode |-
18 17 fveq2d Could not format ( -. A e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  G ) ) : No typesetting found for |- ( -. A e. _V -> ( +g  ( EndoFMnd  A ) ) = ( +g  G ) ) with typecode |-
19 13 18 pm2.61i Could not format ( +g  ( EndoFMnd  A ) ) = ( +g  G ) : No typesetting found for |- ( +g  ( EndoFMnd  A ) ) = ( +g  G ) with typecode |-
20 eqid Could not format ( EndoFMnd  A ) = ( EndoFMnd  A ) : No typesetting found for |- ( EndoFMnd  A ) = ( EndoFMnd  A ) with typecode |-
21 eqid Could not format ( Base  ( EndoFMnd  A ) ) = ( Base  ( EndoFMnd  A ) ) : No typesetting found for |- ( Base  ( EndoFMnd  A ) ) = ( Base  ( EndoFMnd  A ) ) with typecode |-
22 20 21 efmndbas Could not format ( Base  ( EndoFMnd  A ) ) = ( A ^m A ) : No typesetting found for |- ( Base  ( EndoFMnd  A ) ) = ( A ^m A ) with typecode |-
23 2 22 eqtr4i Could not format B = ( Base  ( EndoFMnd  A ) ) : No typesetting found for |- B = ( Base  ( EndoFMnd  A ) ) with typecode |-
24 20 23 6 efmndplusg Could not format ( +g  ( EndoFMnd  A ) ) = ( f e. B , g e. B |-> ( f o. g ) ) : No typesetting found for |- ( +g  ( EndoFMnd  A ) ) = ( f e. B , g e. B |-> ( f o. g ) ) with typecode |-
25 3 19 24 3eqtr2i