Theorem symgfixf1o

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a bijection. (Contributed by AV, 7-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	symgfixf1o	|- ( ( N e. V /\ K e. N ) -> H : Q -1-1-onto-> 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	1 2 3 4	symgfixf1	|- ( K e. N -> H : Q -1-1-> S )
6	5	adantl	|- ( ( N e. V /\ K e. N ) -> H : Q -1-1-> S )
7	1 2 3 4	symgfixfo	|- ( ( N e. V /\ K e. N ) -> H : Q -onto-> S )
8		df-f1o	|- ( H : Q -1-1-onto-> S <-> ( H : Q -1-1-> S /\ H : Q -onto-> S ) )
9	6 7 8	sylanbrc	|- ( ( N e. V /\ K e. N ) -> H : Q -1-1-onto-> S )