Metamath Proof Explorer


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 = ( SymGrp ` A )
symgval.2
|- B = { x | x : A -1-1-onto-> A }
Assertion symgval
|- G = ( ( EndoFMnd ` A ) |`s B )

Proof

Step Hyp Ref Expression
1 symgval.1
 |-  G = ( SymGrp ` A )
2 symgval.2
 |-  B = { x | x : A -1-1-onto-> A }
3 df-symg
 |-  SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) )
4 3 a1i
 |-  ( A e. _V -> SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) )
5 fveq2
 |-  ( x = A -> ( EndoFMnd ` x ) = ( EndoFMnd ` A ) )
6 eqidd
 |-  ( x = A -> h = h )
7 id
 |-  ( x = A -> x = A )
8 6 7 7 f1oeq123d
 |-  ( x = A -> ( h : x -1-1-onto-> x <-> h : A -1-1-onto-> A ) )
9 8 abbidv
 |-  ( x = A -> { h | h : x -1-1-onto-> x } = { h | h : A -1-1-onto-> A } )
10 f1oeq1
 |-  ( h = x -> ( h : A -1-1-onto-> A <-> x : A -1-1-onto-> A ) )
11 10 cbvabv
 |-  { h | h : A -1-1-onto-> A } = { x | x : A -1-1-onto-> A }
12 9 11 eqtrdi
 |-  ( x = A -> { h | h : x -1-1-onto-> x } = { x | x : A -1-1-onto-> A } )
13 12 2 eqtr4di
 |-  ( x = A -> { h | h : x -1-1-onto-> x } = B )
14 5 13 oveq12d
 |-  ( x = A -> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) = ( ( EndoFMnd ` A ) |`s B ) )
15 14 adantl
 |-  ( ( A e. _V /\ x = A ) -> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) = ( ( EndoFMnd ` A ) |`s B ) )
16 id
 |-  ( A e. _V -> A e. _V )
17 ovexd
 |-  ( A e. _V -> ( ( EndoFMnd ` A ) |`s B ) e. _V )
18 nfv
 |-  F/ x A e. _V
19 nfcv
 |-  F/_ x A
20 nfcv
 |-  F/_ x ( EndoFMnd ` A )
21 nfcv
 |-  F/_ x |`s
22 nfab1
 |-  F/_ x { x | x : A -1-1-onto-> A }
23 2 22 nfcxfr
 |-  F/_ x B
24 20 21 23 nfov
 |-  F/_ x ( ( EndoFMnd ` A ) |`s B )
25 4 15 16 17 18 19 24 fvmptdf
 |-  ( A e. _V -> ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) )
26 ress0
 |-  ( (/) |`s B ) = (/)
27 26 a1i
 |-  ( -. A e. _V -> ( (/) |`s B ) = (/) )
28 fvprc
 |-  ( -. A e. _V -> ( EndoFMnd ` A ) = (/) )
29 28 oveq1d
 |-  ( -. A e. _V -> ( ( EndoFMnd ` A ) |`s B ) = ( (/) |`s B ) )
30 fvprc
 |-  ( -. A e. _V -> ( SymGrp ` A ) = (/) )
31 27 29 30 3eqtr4rd
 |-  ( -. A e. _V -> ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B ) )
32 25 31 pm2.61i
 |-  ( SymGrp ` A ) = ( ( EndoFMnd ` A ) |`s B )
33 1 32 eqtri
 |-  G = ( ( EndoFMnd ` A ) |`s B )