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={\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.d	$$⊢D=N\setminus \left\{K\right\}$$
Assertion	symgfixels	$$⊢F\in V\to \left({F\upharpoonright }_D\in S\leftrightarrow \left({F\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}D\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		symgfixf.s	$$⊢S={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
4		symgfixf.d	$$⊢D=N\setminus \left\{K\right\}$$
5	3	eleq2i	$$⊢{F\upharpoonright }_D\in S\leftrightarrow {F\upharpoonright }_D\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
6	5	a1i	$$⊢F\in V\to \left({F\upharpoonright }_D\in S\leftrightarrow {F\upharpoonright }_D\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}\right)$$
7		resexg	$$⊢F\in V\to {F\upharpoonright }_D\in \mathrm{V}$$
8		eqid	$$⊢\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)=\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
10	8 9	elsymgbas2	$$⊢{F\upharpoonright }_D\in \mathrm{V}\to \left({F\upharpoonright }_D\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}\leftrightarrow \left({F\upharpoonright }_D\right):N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\right)$$
11	7 10	syl	$$⊢F\in V\to \left({F\upharpoonright }_D\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}\leftrightarrow \left({F\upharpoonright }_D\right):N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\right)$$
12		eqidd	$$⊢F\in V\to {F\upharpoonright }_D={F\upharpoonright }_D$$
13	4	a1i	$$⊢F\in V\to D=N\setminus \left\{K\right\}$$
14	13	eqcomd	$$⊢F\in V\to N\setminus \left\{K\right\}=D$$
15	12 14 14	f1oeq123d	$$⊢F\in V\to \left(\left({F\upharpoonright }_D\right):N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\leftrightarrow \left({F\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}D\right)$$
16	6 11 15	3bitrd	$$⊢F\in V\to \left({F\upharpoonright }_D\in S\leftrightarrow \left({F\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}D\right)$$