This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )