Step |
Hyp |
Ref |
Expression |
1 |
|
symggrp.1 |
|- G = ( SymGrp ` A ) |
2 |
|
eqid |
|- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) |
3 |
2
|
efmndtset |
|- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` ( EndoFMnd ` A ) ) ) |
4 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
5 |
1 4
|
symgbas |
|- ( Base ` G ) = { f | f : A -1-1-onto-> A } |
6 |
|
fvexd |
|- ( A e. V -> ( Base ` G ) e. _V ) |
7 |
5 6
|
eqeltrrid |
|- ( A e. V -> { f | f : A -1-1-onto-> A } e. _V ) |
8 |
|
eqid |
|- ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) |
9 |
|
eqid |
|- ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( EndoFMnd ` A ) ) |
10 |
8 9
|
resstset |
|- ( { f | f : A -1-1-onto-> A } e. _V -> ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) |
11 |
7 10
|
syl |
|- ( A e. V -> ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) |
12 |
|
eqid |
|- { f | f : A -1-1-onto-> A } = { f | f : A -1-1-onto-> A } |
13 |
1 12
|
symgval |
|- G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) |
14 |
13
|
eqcomi |
|- ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = G |
15 |
14
|
fveq2i |
|- ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( TopSet ` G ) |
16 |
15
|
a1i |
|- ( A e. V -> ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( TopSet ` G ) ) |
17 |
3 11 16
|
3eqtrd |
|- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` G ) ) |