Theorem efmndtopn

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

	Ref	Expression
Hypotheses	efmndtopn.g	No typesetting found for |- G = ( EndoFMnd ` X ) with typecode |-
	efmndtopn.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	efmndtopn	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right){\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		efmndtopn.g	Could not format G = ( EndoFMnd ` X ) : No typesetting found for |- G = ( EndoFMnd ` X ) with typecode |-
2		efmndtopn.b	$$⊢B={\mathrm{Base}}_G$$
3	1	efmndtset	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right)=\mathrm{TopSet}\left(G\right)$$
4	3	oveq1d	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right){\upharpoonright }_{𝑡}B=\mathrm{TopSet}\left(G\right){\upharpoonright }_{𝑡}B$$
5		eqid	$$⊢\mathrm{TopSet}\left(G\right)=\mathrm{TopSet}\left(G\right)$$
6	2 5	topnval	$$⊢\mathrm{TopSet}\left(G\right){\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(G\right)$$
7	4 6	syl6eq	$$⊢X\in V\to {\prod }_{𝑡}\left(X\times \left\{𝒫X\right\}\right){\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(G\right)$$