Theorem symgtopn

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

	Ref	Expression
Hypotheses	symgga.g	⊢ 𝐺 = ( SymGrp ‘ 𝑋 )
	symgga.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	symgtopn	⊢ ( 𝑋 ∈ 𝑉 → ( ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) ↾t 𝐵 ) = ( TopOpen ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		symgga.g	⊢ 𝐺 = ( SymGrp ‘ 𝑋 )
2		symgga.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	1	symgtset	⊢ ( 𝑋 ∈ 𝑉 → ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) = ( TopSet ‘ 𝐺 ) )
4	3	oveq1d	⊢ ( 𝑋 ∈ 𝑉 → ( ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) ↾t 𝐵 ) = ( ( TopSet ‘ 𝐺 ) ↾t 𝐵 ) )
5		eqid	⊢ ( TopSet ‘ 𝐺 ) = ( TopSet ‘ 𝐺 )
6	2 5	topnval	⊢ ( ( TopSet ‘ 𝐺 ) ↾t 𝐵 ) = ( TopOpen ‘ 𝐺 )
7	4 6	eqtrdi	⊢ ( 𝑋 ∈ 𝑉 → ( ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) ↾t 𝐵 ) = ( TopOpen ‘ 𝐺 ) )