Metamath Proof Explorer


Theorem symgtset

Description: The topology of the symmetric group on A . This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just bijections - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by Mario Carneiro, 29-Aug-2015) (Proof revised by AV, 30-Mar-2024.)

Ref Expression
Hypothesis symggrp.1
|- G = ( SymGrp ` A )
Assertion symgtset
|- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` G ) )

Proof

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