Theorem symgfixf

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a function. (Contributed by AV, 4-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	|- P = ( Base ` ( SymGrp ` N ) )
	symgfixf.q	|- Q = { q e. P | ( q ` K ) = K }
	symgfixf.s	|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
	symgfixf.h	|- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
Assertion	symgfixf	|- ( K e. N -> H : Q --> S )

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	|- P = ( Base ` ( SymGrp ` N ) )
2		symgfixf.q	|- Q = { q e. P | ( q ` K ) = K }
3		symgfixf.s	|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
4		symgfixf.h	|- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
5		eqid	|- ( N \ { K } ) = ( N \ { K } )
6	1 2 3 5	symgfixelsi	|- ( ( K e. N /\ q e. Q ) -> ( q |` ( N \ { K } ) ) e. S )
7	6 4	fmptd	|- ( K e. N -> H : Q --> S )