Theorem efmnd0nmnd

Description: Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024)

	Ref	Expression
Assertion	efmnd0nmnd	Could not format assertion : No typesetting found for |- ( EndoFMnd ` (/) ) e. Mnd with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		eqid	Could not format ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) with typecode |-
3	2	efmndmnd	Could not format ( (/) e. _V -> ( EndoFMnd ` (/) ) e. Mnd ) : No typesetting found for |- ( (/) e. _V -> ( EndoFMnd ` (/) ) e. Mnd ) with typecode |-
4	1 3	ax-mp	Could not format ( EndoFMnd ` (/) ) e. Mnd : No typesetting found for |- ( EndoFMnd ` (/) ) e. Mnd with typecode |-