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 𝐺 = ( SymGrp ‘ 𝐴 )
symgval.2 𝐵 = { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
Assertion symgval 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )

Proof

Step Hyp Ref Expression
1 symgval.1 𝐺 = ( SymGrp ‘ 𝐴 )
2 symgval.2 𝐵 = { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
3 df-symg SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) )
4 3 a1i ( 𝐴 ∈ V → SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) ) )
5 fveq2 ( 𝑥 = 𝐴 → ( EndoFMnd ‘ 𝑥 ) = ( EndoFMnd ‘ 𝐴 ) )
6 eqidd ( 𝑥 = 𝐴 = )
7 id ( 𝑥 = 𝐴𝑥 = 𝐴 )
8 6 7 7 f1oeq123d ( 𝑥 = 𝐴 → ( : 𝑥1-1-onto𝑥 : 𝐴1-1-onto𝐴 ) )
9 8 abbidv ( 𝑥 = 𝐴 → { : 𝑥1-1-onto𝑥 } = { : 𝐴1-1-onto𝐴 } )
10 f1oeq1 ( = 𝑥 → ( : 𝐴1-1-onto𝐴𝑥 : 𝐴1-1-onto𝐴 ) )
11 10 cbvabv { : 𝐴1-1-onto𝐴 } = { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
12 9 11 eqtrdi ( 𝑥 = 𝐴 → { : 𝑥1-1-onto𝑥 } = { 𝑥𝑥 : 𝐴1-1-onto𝐴 } )
13 12 2 eqtr4di ( 𝑥 = 𝐴 → { : 𝑥1-1-onto𝑥 } = 𝐵 )
14 5 13 oveq12d ( 𝑥 = 𝐴 → ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
15 14 adantl ( ( 𝐴 ∈ V ∧ 𝑥 = 𝐴 ) → ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
16 id ( 𝐴 ∈ V → 𝐴 ∈ V )
17 ovexd ( 𝐴 ∈ V → ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ∈ V )
18 nfv 𝑥 𝐴 ∈ V
19 nfcv 𝑥 𝐴
20 nfcv 𝑥 ( EndoFMnd ‘ 𝐴 )
21 nfcv 𝑥s
22 nfab1 𝑥 { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
23 2 22 nfcxfr 𝑥 𝐵
24 20 21 23 nfov 𝑥 ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )
25 4 15 16 17 18 19 24 fvmptdf ( 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
26 ress0 ( ∅ ↾s 𝐵 ) = ∅
27 26 a1i ( ¬ 𝐴 ∈ V → ( ∅ ↾s 𝐵 ) = ∅ )
28 fvprc ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ )
29 28 oveq1d ( ¬ 𝐴 ∈ V → ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) = ( ∅ ↾s 𝐵 ) )
30 fvprc ( ¬ 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ∅ )
31 27 29 30 3eqtr4rd ( ¬ 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
32 25 31 pm2.61i ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )
33 1 32 eqtri 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )