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) (Proof shortened by AV, 14-Aug-2024)

	Ref	Expression
Hypotheses	symgplusg.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgplusg.2	$$⊢B=A^A$$
	symgplusg.3	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	symgplusg	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$

Proof

Step	Hyp	Ref	Expression
1		symgplusg.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgplusg.2	$$⊢B=A^A$$
3		symgplusg.3	$$⊢\underset{\dot{}}{+}={+}_G$$
4		f1osetex	$$⊢\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	ax-mp	Could not format ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) : No typesetting found for |- ( +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	eqtri	Could not format ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) : No typesetting found for |- ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) with typecode |-
14		eqid	Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
15		eqid	Could not format ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
16	14 15	efmndbas	Could not format ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A ) with typecode |-
17	2 16	eqtr4i	Could not format B = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- B = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
18	14 17 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 |-
19	3 13 18	3eqtr2i	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$