This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) ↾_{𝑡} B = TopOpen (G)$

Step	Hyp	Ref	Expression
1		efmndtopn.g	$⊢ G = EndoFMnd (X)$
2		efmndtopn.b	$⊢ B = {Base}_{G}$
3	1	efmndtset	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) = TopSet (G)$
4	3	oveq1d	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) ↾_{𝑡} B = TopSet (G) ↾_{𝑡} B$
5		eqid	$⊢ TopSet (G) = TopSet (G)$
6	2 5	topnval	$⊢ TopSet (G) ↾_{𝑡} B = TopOpen (G)$
7	4 6	eqtrdi	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) ↾_{𝑡} B = TopOpen (G)$