Theorem symgtopn

Description: The topology of the symmetric group on A . (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	symgga.g	|- G = ( SymGrp ` X )
	symgga.b	|- B = ( Base ` G )
Assertion	symgtopn	|- ( X e. V -> ( ( Xt_ ` ( X X. { ~P X } ) ) |`t B ) = ( TopOpen ` G ) )

Proof

Step	Hyp	Ref	Expression
1		symgga.g	|- G = ( SymGrp ` X )
2		symgga.b	|- B = ( Base ` G )
3	1	symgtset	|- ( X e. V -> ( Xt_ ` ( X X. { ~P X } ) ) = ( TopSet ` G ) )
4	3	oveq1d	|- ( X e. V -> ( ( Xt_ ` ( X X. { ~P X } ) ) |`t B ) = ( ( TopSet ` G ) |`t B ) )
5		eqid	|- ( TopSet ` G ) = ( TopSet ` G )
6	2 5	topnval	|- ( ( TopSet ` G ) |`t B ) = ( TopOpen ` G )
7	4 6	eqtrdi	|- ( X e. V -> ( ( Xt_ ` ( X X. { ~P X } ) ) |`t B ) = ( TopOpen ` G ) )