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