This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )