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