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 G=SymGrpX
symgga.b B=BaseG
Assertion symgtopn XV𝑡X×𝒫X𝑡B=TopOpenG

Proof

Step Hyp Ref Expression
1 symgga.g G=SymGrpX
2 symgga.b B=BaseG
3 1 symgtset XV𝑡X×𝒫X=TopSetG
4 3 oveq1d XV𝑡X×𝒫X𝑡B=TopSetG𝑡B
5 eqid TopSetG=TopSetG
6 2 5 topnval TopSetG𝑡B=TopOpenG
7 4 6 eqtrdi XV𝑡X×𝒫X𝑡B=TopOpenG