Theorem symgfixels

Description: The restriction of a permutation to a set with one element removed is an element of the restricted symmetric group if the restriction is a 1-1 onto 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.d	|- D = ( N \ { K } )
Assertion	symgfixels	|- ( F e. V -> ( ( F |` D ) e. S <-> ( F |` D ) : D -1-1-onto-> D ) )

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.d	|- D = ( N \ { K } )
5	3	eleq2i	|- ( ( F |` D ) e. S <-> ( F |` D ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) )
6	5	a1i	|- ( F e. V -> ( ( F |` D ) e. S <-> ( F |` D ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) ) )
7		resexg	|- ( F e. V -> ( F |` D ) e. _V )
8		eqid	|- ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
9		eqid	|- ( Base ` ( SymGrp ` ( N \ { K } ) ) ) = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
10	8 9	elsymgbas2	|- ( ( F |` D ) e. _V -> ( ( F |` D ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) <-> ( F |` D ) : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) ) )
11	7 10	syl	|- ( F e. V -> ( ( F |` D ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) <-> ( F |` D ) : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) ) )
12		eqidd	|- ( F e. V -> ( F |` D ) = ( F |` D ) )
13	4	a1i	|- ( F e. V -> D = ( N \ { K } ) )
14	13	eqcomd	|- ( F e. V -> ( N \ { K } ) = D )
15	12 14 14	f1oeq123d	|- ( F e. V -> ( ( F |` D ) : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) <-> ( F |` D ) : D -1-1-onto-> D ) )
16	6 11 15	3bitrd	|- ( F e. V -> ( ( F |` D ) e. S <-> ( F |` D ) : D -1-1-onto-> D ) )