Theorem efmndbasabf

Description: The base set of the monoid of endofunctions on class A is the set of functions from A into itself. (Contributed by AV, 29-Mar-2024)

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

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	1 2	efmndbas	$$⊢B=A^A$$
4		mapvalg	$$⊢\left(A\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to A^A=\left\{f|f:A⟶A\right\}$$
5	4	anidms	$$⊢A\in \mathrm{V}\to A^A=\left\{f|f:A⟶A\right\}$$
6	3 5	syl5eq	$$⊢A\in \mathrm{V}\to B=\left\{f|f:A⟶A\right\}$$
7		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
8	7	eqcomi	$$⊢{\mathrm{Base}}_{\varnothing }=\varnothing$$
9		fvprc	Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) with typecode |-
10	1 9	syl5eq	$$⊢\neg A\in \mathrm{V}\to G=\varnothing$$
11	10	fveq2d	$$⊢\neg A\in \mathrm{V}\to {\mathrm{Base}}_G={\mathrm{Base}}_{\varnothing }$$
12	2 11	syl5eq	$$⊢\neg A\in \mathrm{V}\to B={\mathrm{Base}}_{\varnothing }$$
13		mapprc	$$⊢\neg A\in \mathrm{V}\to \left\{f|f:A⟶A\right\}=\varnothing$$
14	8 12 13	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to B=\left\{f|f:A⟶A\right\}$$
15	6 14	pm2.61i	$$⊢B=\left\{f|f:A⟶A\right\}$$