Theorem efmnd

Description: The monoid of endofunctions on set A . (Contributed by AV, 25-Jan-2024)

	Ref	Expression
Hypotheses	efmnd.1	$$⊢G=\mathrm{EndoFMnd}\left(A\right)$$
	efmnd.2	$$⊢B=A^A$$
	efmnd.3	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$
	efmnd.4	$$⊢J={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
Assertion	efmnd	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		efmnd.1	$$⊢G=\mathrm{EndoFMnd}\left(A\right)$$
2		efmnd.2	$$⊢B=A^A$$
3		efmnd.3	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$
4		efmnd.4	$$⊢J={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
5		elex	$$⊢A\in V\to A\in \mathrm{V}$$
6		ovexd	$$⊢a=A\to a^a\in \mathrm{V}$$
7		id	$$⊢b=a^a\to b=a^a$$
8		id	$$⊢a=A\to a=A$$
9	8 8	oveq12d	$$⊢a=A\to a^a=A^A$$
10	9 2	eqtr4di	$$⊢a=A\to a^a=B$$
11	7 10	sylan9eqr	$$⊢\left(a=A\wedge b=a^a\right)\to b=B$$
12	11	opeq2d	$$⊢\left(a=A\wedge b=a^a\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩$$
13		eqidd	$$⊢\left(a=A\wedge b=a^a\right)\to f\circ g=f\circ g$$
14	11 11 13	mpoeq123dv	$$⊢\left(a=A\wedge b=a^a\right)\to \left(f\in b,g\in b⟼f\circ g\right)=\left(f\in B,g\in B⟼f\circ g\right)$$
15	14 3	eqtr4di	$$⊢\left(a=A\wedge b=a^a\right)\to \left(f\in b,g\in b⟼f\circ g\right)=\underset{\dot{}}{+}$$
16	15	opeq2d	$$⊢\left(a=A\wedge b=a^a\right)\to ⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩$$
17		simpl	$$⊢\left(a=A\wedge b=a^a\right)\to a=A$$
18		pweq	$$⊢a=A\to 𝒫a=𝒫A$$
19	18	sneqd	$$⊢a=A\to \left\{𝒫a\right\}=\left\{𝒫A\right\}$$
20	19	adantr	$$⊢\left(a=A\wedge b=a^a\right)\to \left\{𝒫a\right\}=\left\{𝒫A\right\}$$
21	17 20	xpeq12d	$$⊢\left(a=A\wedge b=a^a\right)\to a\times \left\{𝒫a\right\}=A\times \left\{𝒫A\right\}$$
22	21	fveq2d	$$⊢\left(a=A\wedge b=a^a\right)\to {\prod }_{𝑡}\left(a\times \left\{𝒫a\right\}\right)={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
23	22 4	eqtr4di	$$⊢\left(a=A\wedge b=a^a\right)\to {\prod }_{𝑡}\left(a\times \left\{𝒫a\right\}\right)=J$$
24	23	opeq2d	$$⊢\left(a=A\wedge b=a^a\right)\to ⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(a\times \left\{𝒫a\right\}\right)⟩=⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩$$
25	12 16 24	tpeq123d	$$⊢\left(a=A\wedge b=a^a\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(a\times \left\{𝒫a\right\}\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
26	6 25	csbied	$$⊢a=A\to ⦋\left(a^a\right)/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(a\times \left\{𝒫a\right\}\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
27		df-efmnd	$$⊢\mathrm{EndoFMnd}=\left(a\in \mathrm{V}⟼⦋\left(a^a\right)/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(a\times \left\{𝒫a\right\}\right)⟩\right\}\right)$$
28		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\in \mathrm{V}$$
29	26 27 28	fvmpt	$$⊢A\in \mathrm{V}\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
30	5 29	syl	$$⊢A\in V\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
31	1 30	eqtrid	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$