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=\mathrm{SymGrp}\left(A\right)$$
Assertion	symgtset	$$⊢A\in V\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		eqid	Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
3	2	efmndtset	Could not format ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` ( EndoFMnd ` A ) ) ) : No typesetting found for |- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` ( EndoFMnd ` A ) ) ) with typecode |-
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	1 4	symgbas	$$⊢{\mathrm{Base}}_G=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
6		fvexd	$$⊢A\in V\to {\mathrm{Base}}_G\in \mathrm{V}$$
7	5 6	eqeltrrid	$$⊢A\in V\to \left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\in \mathrm{V}$$
8		eqid	Could not format ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) with typecode |-
9		eqid	Could not format ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( EndoFMnd ` A ) ) with typecode |-
10	8 9	resstset	Could not format ( { f | f : A -1-1-onto-> A } e. _V -> ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( { f | f : A -1-1-onto-> A } e. _V -> ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) with typecode |-
11	7 10	syl	Could not format ( A e. V -> ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( A e. V -> ( TopSet ` ( EndoFMnd ` A ) ) = ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) with typecode |-
12		eqid	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
13	1 12	symgval	Could not format G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) with typecode |-
14	13	eqcomi	Could not format ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = G : No typesetting found for |- ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = G with typecode |-
15	14	fveq2i	Could not format ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( TopSet ` G ) : No typesetting found for |- ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( TopSet ` G ) with typecode |-
16	15	a1i	Could not format ( A e. V -> ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( TopSet ` G ) ) : No typesetting found for |- ( A e. V -> ( TopSet ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( TopSet ` G ) ) with typecode |-
17	3 11 16	3eqtrd	$$⊢A\in V\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(G\right)$$