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 ) |