Theorem symgfixf1o

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a bijection. (Contributed by AV, 7-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	symgfixf1o	$$⊢\left(N\in V\wedge K\in N\right)\to H:Q\underset{1-1\; onto}{⟶}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	1 2 3 4	symgfixf1	$$⊢K\in N\to H:Q\underset{1-1}{⟶}S$$
6	5	adantl	$$⊢\left(N\in V\wedge K\in N\right)\to H:Q\underset{1-1}{⟶}S$$
7	1 2 3 4	symgfixfo	$$⊢\left(N\in V\wedge K\in N\right)\to H:Q\underset{onto}{⟶}S$$
8		df-f1o	$$⊢H:Q\underset{1-1\; onto}{⟶}S\leftrightarrow \left(H:Q\underset{1-1}{⟶}S\wedge H:Q\underset{onto}{⟶}S\right)$$
9	6 7 8	sylanbrc	$$⊢\left(N\in V\wedge K\in N\right)\to H:Q\underset{1-1\; onto}{⟶}S$$