Theorem symgval

Description: The value of the symmetric group function at A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 12-Jan-2015) (Revised by AV, 28-Mar-2024)

	Ref	Expression
Hypotheses	symgval.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgval.2	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
Assertion	symgval	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$

Proof

Step	Hyp	Ref	Expression
1		symgval.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgval.2	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
3		df-symg	$$⊢\mathrm{SymGrp}=\left(x\in \mathrm{V}⟼\mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}\right)$$
4	3	a1i	$$⊢A\in \mathrm{V}\to \mathrm{SymGrp}=\left(x\in \mathrm{V}⟼\mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}\right)$$
5		fveq2	$$⊢x=A\to \mathrm{EndoFMnd}\left(x\right)=\mathrm{EndoFMnd}\left(A\right)$$
6		eqidd	$$⊢x=A\to h=h$$
7		id	$$⊢x=A\to x=A$$
8	6 7 7	f1oeq123d	$$⊢x=A\to \left(h:x\underset{1-1\; onto}{⟶}x\leftrightarrow h:A\underset{1-1\; onto}{⟶}A\right)$$
9	8	abbidv	$$⊢x=A\to \left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}=\left\{h|h:A\underset{1-1\; onto}{⟶}A\right\}$$
10		f1oeq1	$$⊢h=x\to \left(h:A\underset{1-1\; onto}{⟶}A\leftrightarrow x:A\underset{1-1\; onto}{⟶}A\right)$$
11	10	cbvabv	$$⊢\left\{h|h:A\underset{1-1\; onto}{⟶}A\right\}=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
12	9 11	eqtrdi	$$⊢x=A\to \left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
13	12 2	eqtr4di	$$⊢x=A\to \left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}=B$$
14	5 13	oveq12d	$$⊢x=A\to \mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$
15	14	adantl	$$⊢\left(A\in \mathrm{V}\wedge x=A\right)\to \mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$
16		id	$$⊢A\in \mathrm{V}\to A\in \mathrm{V}$$
17		ovexd	$$⊢A\in \mathrm{V}\to \mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B\in \mathrm{V}$$
18		nfv	$$⊢ℲxA\in \mathrm{V}$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{EndoFMnd}\left(A\right)$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}x{\upharpoonright }_{𝑠}$$
22		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
23	2 22	nfcxfr	$$⊢\underset{\_}{Ⅎ}xB$$
24	20 21 23	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B\right)$$
25	4 15 16 17 18 19 24	fvmptdf	$$⊢A\in \mathrm{V}\to \mathrm{SymGrp}\left(A\right)=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$
26		ress0	$$⊢\varnothing {\upharpoonright }_{𝑠}B=\varnothing$$
27	26	a1i	$$⊢\neg A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑠}B=\varnothing$$
28		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{EndoFMnd}\left(A\right)=\varnothing$$
29	28	oveq1d	$$⊢\neg A\in \mathrm{V}\to \mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B=\varnothing {\upharpoonright }_{𝑠}B$$
30		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{SymGrp}\left(A\right)=\varnothing$$
31	27 29 30	3eqtr4rd	$$⊢\neg A\in \mathrm{V}\to \mathrm{SymGrp}\left(A\right)=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$
32	25 31	pm2.61i	$$⊢\mathrm{SymGrp}\left(A\right)=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$
33	1 32	eqtri	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$