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={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	symgfixf.q	$$⊢Q=\left\{q\in P|q\left(K\right)=K\right\}$$
Assertion	symgfixelq	$$⊢F\in V\to \left(F\in Q\leftrightarrow \left(F:N\underset{1-1\; onto}{⟶}N\wedge F\left(K\right)=K\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
2		symgfixf.q	$$⊢Q=\left\{q\in P|q\left(K\right)=K\right\}$$
3		fveq1	$$⊢f=F\to f\left(K\right)=F\left(K\right)$$
4	3	eqeq1d	$$⊢f=F\to \left(f\left(K\right)=K\leftrightarrow F\left(K\right)=K\right)$$
5		fveq1	$$⊢q=f\to q\left(K\right)=f\left(K\right)$$
6	5	eqeq1d	$$⊢q=f\to \left(q\left(K\right)=K\leftrightarrow f\left(K\right)=K\right)$$
7	6	cbvrabv	$$⊢\left\{q\in P|q\left(K\right)=K\right\}=\left\{f\in P|f\left(K\right)=K\right\}$$
8	2 7	eqtri	$$⊢Q=\left\{f\in P|f\left(K\right)=K\right\}$$
9	4 8	elrab2	$$⊢F\in Q\leftrightarrow \left(F\in P\wedge F\left(K\right)=K\right)$$
10		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
11	10 1	elsymgbas2	$$⊢F\in V\to \left(F\in P\leftrightarrow F:N\underset{1-1\; onto}{⟶}N\right)$$
12	11	anbi1d	$$⊢F\in V\to \left(\left(F\in P\wedge F\left(K\right)=K\right)\leftrightarrow \left(F:N\underset{1-1\; onto}{⟶}N\wedge F\left(K\right)=K\right)\right)$$
13	9 12	bitrid	$$⊢F\in V\to \left(F\in Q\leftrightarrow \left(F:N\underset{1-1\; onto}{⟶}N\wedge F\left(K\right)=K\right)\right)$$