This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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