Theorem efmndtopn

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

	Ref	Expression
Hypotheses	efmndtopn.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝑋 )
	efmndtopn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	efmndtopn	⊢ ( 𝑋 ∈ 𝑉 → ( ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) ↾t 𝐵 ) = ( TopOpen ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		efmndtopn.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝑋 )
2		efmndtopn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	1	efmndtset	⊢ ( 𝑋 ∈ 𝑉 → ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) = ( TopSet ‘ 𝐺 ) )
4	3	oveq1d	⊢ ( 𝑋 ∈ 𝑉 → ( ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) ↾t 𝐵 ) = ( ( TopSet ‘ 𝐺 ) ↾t 𝐵 ) )
5		eqid	⊢ ( TopSet ‘ 𝐺 ) = ( TopSet ‘ 𝐺 )
6	2 5	topnval	⊢ ( ( TopSet ‘ 𝐺 ) ↾t 𝐵 ) = ( TopOpen ‘ 𝐺 )
7	4 6	eqtrdi	⊢ ( 𝑋 ∈ 𝑉 → ( ( ∏t ‘ ( 𝑋 × { 𝒫 𝑋 } ) ) ↾t 𝐵 ) = ( TopOpen ‘ 𝐺 ) )