Metamath Proof Explorer


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