Theorem efmnd

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

	Ref	Expression
Hypotheses	efmnd.1	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	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	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
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	syl6eqr	$$⊢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	syl6eqr	$$⊢\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	syl6eqr	$$⊢\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	Could not format EndoFMnd = ( a e. _V |-> [_ ( a ^m a ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( a X. { ~P a } ) ) >. } ) : No typesetting found for |- EndoFMnd = ( a e. _V |-> [_ ( a ^m a ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( a X. { ~P a } ) ) >. } ) with typecode |-
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	Could not format ( A e. _V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( A e. _V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
30	5 29	syl	Could not format ( A e. V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( A e. V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
31	1 30	syl5eq	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$