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	Could not format assertion : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s B ) with typecode |-

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	Could not format SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) : No typesetting found for |- SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) with typecode |-
4	3	a1i	Could not format ( A e. _V -> SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) ) : No typesetting found for |- ( A e. _V -> SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) ) with typecode |-
5		fveq2	Could not format ( x = A -> ( EndoFMnd ` x ) = ( EndoFMnd ` A ) ) : No typesetting found for |- ( x = A -> ( EndoFMnd ` x ) = ( EndoFMnd ` A ) ) with typecode |-
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	Could not format ( x = A -> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) = ( ( EndoFMnd ` A ) |`s B ) ) : No typesetting found for |- ( x = A -> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) = ( ( EndoFMnd ` A ) |`s B ) ) with typecode |-
15	14	adantl	Could not format ( ( A e. _V /\ x = A ) -> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) = ( ( EndoFMnd ` A ) |`s B ) ) : No typesetting found for |- ( ( A e. _V /\ x = A ) -> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) = ( ( EndoFMnd ` A ) |`s B ) ) with typecode |-
16		id	$$⊢A\in \mathrm{V}\to A\in \mathrm{V}$$
17		ovexd	Could not format ( A e. _V -> ( ( EndoFMnd ` A ) |`s B ) e. _V ) : No typesetting found for |- ( A e. _V -> ( ( EndoFMnd ` A ) |`s B ) e. _V ) with typecode |-
18		nfv	$$⊢ℲxA\in \mathrm{V}$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
20		nfcv	Could not format F/_ x ( EndoFMnd ` A ) : No typesetting found for |- F/_ x ( EndoFMnd ` A ) with typecode |-
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	Could not format F/_ x ( ( EndoFMnd ` A ) |`s B ) : No typesetting found for |- F/_ x ( ( EndoFMnd ` A ) |`s B ) with typecode |-
25	4 15 16 17 18 19 24	fvmptdf	Could not format ( A e. _V -> ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) ) : No typesetting found for |- ( A e. _V -> ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) ) with typecode |-
26		ress0	$$⊢\varnothing {\upharpoonright }_{𝑠}B=\varnothing$$
27	26	a1i	$$⊢\neg A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑠}B=\varnothing$$
28		fvprc	Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) with typecode |-
29	28	oveq1d	Could not format ( -. A e. _V -> ( ( EndoFMnd ` A ) |`s B ) = ( (/) |`s B ) ) : No typesetting found for |- ( -. A e. _V -> ( ( EndoFMnd ` A ) |`s B ) = ( (/) |`s B ) ) with typecode |-
30		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{SymGrp}\left(A\right)=\varnothing$$
31	27 29 30	3eqtr4rd	Could not format ( -. A e. _V -> ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) ) : No typesetting found for |- ( -. A e. _V -> ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) ) with typecode |-
32	25 31	pm2.61i	Could not format ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) : No typesetting found for |- ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) with typecode |-
33	1 32	eqtri	Could not format G = ( ( EndoFMnd ` A ) |`s B ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s B ) with typecode |-