Theorem efmndbas0

Description: The base set of the monoid of endofunctions on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Jan-2024) (Proof shortened by AV, 31-Mar-2024)

	Ref	Expression
Assertion	efmndbas0	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\varnothing \right)}=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{EndoFMnd}\left(\varnothing \right)=\mathrm{EndoFMnd}\left(\varnothing \right)$$
2		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\varnothing \right)}={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\varnothing \right)}$$
3	1 2	efmndbas	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\varnothing \right)}={\varnothing }^{\varnothing }$$
4		0map0sn0	$$⊢{\varnothing }^{\varnothing }=\left\{\varnothing \right\}$$
5	3 4	eqtri	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\varnothing \right)}=\left\{\varnothing \right\}$$