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

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