Theorem 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	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion	efmndtset	$$⊢A\in V\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		fvex	$$⊢{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)\in \mathrm{V}$$
3		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A^A⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A^A⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}$$
4	3	topgrptset	$$⊢{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)\in \mathrm{V}\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A^A⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}\right)$$
5	2 4	ax-mp	$$⊢{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A^A⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}\right)$$
6		eqid	$$⊢A^A=A^A$$
7		eqid	$$⊢\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)=\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)$$
8		eqid	$$⊢{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
9	1 6 7 8	efmnd	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A^A⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}$$
10	9	fveq2d	$$⊢A\in V\to \mathrm{TopSet}\left(G\right)=\mathrm{TopSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A^A⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}\right)$$
11	5 10	eqtr4id	$$⊢A\in V\to {\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)=\mathrm{TopSet}\left(G\right)$$