Theorem symgga

Description: The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015)

	Ref	Expression
Hypotheses	symgga.g	|- G = ( SymGrp ` X )
	symgga.b	|- B = ( Base ` G )
	symgga.f	|- F = ( f e. B , x e. X |-> ( f ` x ) )
Assertion	symgga	|- ( X e. V -> F e. ( G GrpAct X ) )

Proof

Step	Hyp	Ref	Expression
1		symgga.g	|- G = ( SymGrp ` X )
2		symgga.b	|- B = ( Base ` G )
3		symgga.f	|- F = ( f e. B , x e. X |-> ( f ` x ) )
4	1	symggrp	|- ( X e. V -> G e. Grp )
5	2	idghm	|- ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )
6		fvresi	|- ( f e. B -> ( ( _I |` B ) ` f ) = f )
7	6	adantr	|- ( ( f e. B /\ x e. X ) -> ( ( _I |` B ) ` f ) = f )
8	7	fveq1d	|- ( ( f e. B /\ x e. X ) -> ( ( ( _I |` B ) ` f ) ` x ) = ( f ` x ) )
9	8	mpoeq3ia	|- ( f e. B , x e. X |-> ( ( ( _I |` B ) ` f ) ` x ) ) = ( f e. B , x e. X |-> ( f ` x ) )
10	3 9	eqtr4i	|- F = ( f e. B , x e. X |-> ( ( ( _I |` B ) ` f ) ` x ) )
11	2 1 10	lactghmga	|- ( ( _I |` B ) e. ( G GrpHom G ) -> F e. ( G GrpAct X ) )
12	4 5 11	3syl	|- ( X e. V -> F e. ( G GrpAct X ) )