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