Theorem efmndtopn

Description: The topology of the monoid of endofunctions on A . (Contributed by AV, 31-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		efmndtopn.g	|- G = ( EndoFMnd ` X )
2		efmndtopn.b	|- B = ( Base ` G )
3	1	efmndtset	|- ( 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 ) )