Theorem symgtopn

Description: The topology of the symmetric group on A . (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	symgga.g	$$⊢G=\mathrm{SymGrp}\left(X\right)$$
	symgga.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgtopn	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right){\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		symgga.g	$$⊢G=\mathrm{SymGrp}\left(X\right)$$
2		symgga.b	$$⊢B={\mathrm{Base}}_G$$
3	1	symgtset	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right)=\mathrm{TopSet}\left(G\right)$$
4	3	oveq1d	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right){\upharpoonright }_{𝑡}B=\mathrm{TopSet}\left(G\right){\upharpoonright }_{𝑡}B$$
5		eqid	$$⊢\mathrm{TopSet}\left(G\right)=\mathrm{TopSet}\left(G\right)$$
6	2 5	topnval	$$⊢\mathrm{TopSet}\left(G\right){\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(G\right)$$
7	4 6	eqtrdi	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right){\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(G\right)$$