Theorem symgfixf

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a function. (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\}$$
	symgfixf.s	$$⊢S={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
	symgfixf.h	$$⊢H=\left(q\in Q⟼{q\upharpoonright }_{\left(N\setminus \left\{K\right\}\right)}\right)$$
Assertion	symgfixf	$$⊢K\in N\to H:Q⟶S$$

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		symgfixf.s	$$⊢S={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
4		symgfixf.h	$$⊢H=\left(q\in Q⟼{q\upharpoonright }_{\left(N\setminus \left\{K\right\}\right)}\right)$$
5		eqid	$$⊢N\setminus \left\{K\right\}=N\setminus \left\{K\right\}$$
6	1 2 3 5	symgfixelsi	$$⊢\left(K\in N\wedge q\in Q\right)\to {q\upharpoonright }_{\left(N\setminus \left\{K\right\}\right)}\in S$$
7	6 4	fmptd	$$⊢K\in N\to H:Q⟶S$$