Theorem symgfixelq

Description: A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	|- P = ( Base ` ( SymGrp ` N ) )
	symgfixf.q	|- Q = { q e. P | ( q ` K ) = K }
Assertion	symgfixelq	|- ( F e. V -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	|- P = ( Base ` ( SymGrp ` N ) )
2		symgfixf.q	|- Q = { q e. P | ( q ` K ) = K }
3		fveq1	|- ( f = F -> ( f ` K ) = ( F ` K ) )
4	3	eqeq1d	|- ( f = F -> ( ( f ` K ) = K <-> ( F ` K ) = K ) )
5		fveq1	|- ( q = f -> ( q ` K ) = ( f ` K ) )
6	5	eqeq1d	|- ( q = f -> ( ( q ` K ) = K <-> ( f ` K ) = K ) )
7	6	cbvrabv	|- { q e. P | ( q ` K ) = K } = { f e. P | ( f ` K ) = K }
8	2 7	eqtri	|- Q = { f e. P | ( f ` K ) = K }
9	4 8	elrab2	|- ( F e. Q <-> ( F e. P /\ ( F ` K ) = K ) )
10		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
11	10 1	elsymgbas2	|- ( F e. V -> ( F e. P <-> F : N -1-1-onto-> N ) )
12	11	anbi1d	|- ( F e. V -> ( ( F e. P /\ ( F ` K ) = K ) <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )
13	9 12	bitrid	|- ( F e. V -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )