Metamath Proof Explorer


Theorem symgtset

Description: The topology of the symmetric group on A . This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just bijections - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by Mario Carneiro, 29-Aug-2015) (Proof revised by AV, 30-Mar-2024.)

Ref Expression
Hypothesis symggrp.1 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion symgtset ( 𝐴𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 symggrp.1 𝐺 = ( SymGrp ‘ 𝐴 )
2 eqid ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ 𝐴 )
3 2 efmndtset ( 𝐴𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) )
4 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 1 4 symgbas ( Base ‘ 𝐺 ) = { 𝑓𝑓 : 𝐴1-1-onto𝐴 }
6 fvexd ( 𝐴𝑉 → ( Base ‘ 𝐺 ) ∈ V )
7 5 6 eqeltrrid ( 𝐴𝑉 → { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ∈ V )
8 eqid ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } )
9 eqid ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) )
10 8 9 resstset ( { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ∈ V → ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ) ) )
11 7 10 syl ( 𝐴𝑉 → ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ) ) )
12 eqid { 𝑓𝑓 : 𝐴1-1-onto𝐴 } = { 𝑓𝑓 : 𝐴1-1-onto𝐴 }
13 1 12 symgval 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } )
14 13 eqcomi ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ) = 𝐺
15 14 fveq2i ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ) ) = ( TopSet ‘ 𝐺 )
16 15 a1i ( 𝐴𝑉 → ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓𝑓 : 𝐴1-1-onto𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )
17 3 11 16 3eqtrd ( 𝐴𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )