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	Could not format assertion : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	Could not format ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) with typecode |-
2		eqid	Could not format ( Base ` ( EndoFMnd ` (/) ) ) = ( Base ` ( EndoFMnd ` (/) ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = ( Base ` ( EndoFMnd ` (/) ) ) with typecode |-
3	1 2	efmndbas	Could not format ( Base ` ( EndoFMnd ` (/) ) ) = ( (/) ^m (/) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = ( (/) ^m (/) ) with typecode |-
4		0map0sn0	$$⊢{\varnothing }^{\varnothing }=\left\{\varnothing \right\}$$
5	3 4	eqtri	Could not format ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } with typecode |-