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	$$⊢\mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(A\right)$$
3	2	efmndtset	$$⊢A\in V\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right)\right)$$
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	$$⊢\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
9		eqid	$$⊢\mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right)\right)=\mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right)\right)$$
10	8 9	resstset	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\in \mathrm{V}\to \mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right)\right)=\mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)$$
11	7 10	syl	$$⊢A\in V\to \mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right)\right)=\mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)$$
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	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
14	13	eqcomi	$$⊢\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=G$$
15	14	fveq2i	$$⊢\mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)=\mathrm{TopSet}\left(G\right)$$
16	15	a1i	$$⊢A\in V\to \mathrm{TopSet}\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)=\mathrm{TopSet}\left(G\right)$$
17	3 11 16	3eqtrd	$$⊢A\in V\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(G\right)$$