efmndtset

Description: The topology of the monoid of endofunctions on A . This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024)

		Ref	Expression
	Hypothesis	efmndtset.g	$⊢ G = EndoFMnd (A)$
	Assertion	efmndtset	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) = TopSet (G)$

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	$⊢ G = EndoFMnd (A)$
2		fvex	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) \in V$
3		eqid	$⊢ \{⟨{Base}_{ndx}, A^{A}⟩, ⟨+_{ndx}, (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (A \times \{𝒫 A\})⟩\} = \{⟨{Base}_{ndx}, A^{A}⟩, ⟨+_{ndx}, (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (A \times \{𝒫 A\})⟩\}$
4	3	topgrptset	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) = TopSet (\{⟨{Base}_{ndx}, A^{A}⟩, ⟨+_{ndx}, (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (A \times \{𝒫 A\})⟩\})$
5	2 4	ax-mp	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) = TopSet (\{⟨{Base}_{ndx}, A^{A}⟩, ⟨+_{ndx}, (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (A \times \{𝒫 A\})⟩\})$
6		eqid	$⊢ A^{A} = A^{A}$
7		eqid	$⊢ (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) = (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)$
8		eqid	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) = \prod_{𝑡} (A \times \{𝒫 A\})$
9	1 6 7 8	efmnd	$⊢ A \in V \to G = \{⟨{Base}_{ndx}, A^{A}⟩, ⟨+_{ndx}, (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (A \times \{𝒫 A\})⟩\}$
10	9	fveq2d	$⊢ A \in V \to TopSet (G) = TopSet (\{⟨{Base}_{ndx}, A^{A}⟩, ⟨+_{ndx}, (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (A \times \{𝒫 A\})⟩\})$
11	5 10	eqtr4id	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) = TopSet (G)$

Metamath Proof Explorer

Theorem efmndtset

Proof