Theorem efmndbas

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

	Ref	Expression
Hypotheses	efmndbas.g	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmndbas.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	efmndbas	$$⊢B=A^A$$

Proof

Step	Hyp	Ref	Expression
1		efmndbas.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		efmndbas.b	$$⊢B={\mathrm{Base}}_G$$
3		ovex	$$⊢A^A\in \mathrm{V}$$
4		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\}$$
5	4	topgrpbas	$$⊢A^A\in \mathrm{V}\to A^A={\mathrm{Base}}_{\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\}}$$
6	3 5	mp1i	$$⊢A\in \mathrm{V}\to A^A={\mathrm{Base}}_{\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\}}$$
7		eqid	$$⊢A^A=A^A$$
8		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)$$
9		eqid	$$⊢{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
10	1 7 8 9	efmnd	$$⊢A\in \mathrm{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\}$$
11	10	fveq2d	$$⊢A\in \mathrm{V}\to {\mathrm{Base}}_G={\mathrm{Base}}_{\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\}}$$
12	6 11	eqtr4d	$$⊢A\in \mathrm{V}\to A^A={\mathrm{Base}}_G$$
13		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
14		reldmmap	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$
15	14	ovprc1	$$⊢\neg A\in \mathrm{V}\to A^A=\varnothing$$
16		fvprc	Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) with typecode |-
17	1 16	syl5eq	$$⊢\neg A\in \mathrm{V}\to G=\varnothing$$
18	17	fveq2d	$$⊢\neg A\in \mathrm{V}\to {\mathrm{Base}}_G={\mathrm{Base}}_{\varnothing }$$
19	13 15 18	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to A^A={\mathrm{Base}}_G$$
20	12 19	pm2.61i	$$⊢A^A={\mathrm{Base}}_G$$
21	2 20	eqtr4i	$$⊢B=A^A$$