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	⊢ ( EndoFMnd ‘ ∅ ) ∈ Mnd

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eqid	⊢ ( EndoFMnd ‘ ∅ ) = ( EndoFMnd ‘ ∅ )
3	2	efmndmnd	⊢ ( ∅ ∈ V → ( EndoFMnd ‘ ∅ ) ∈ Mnd )
4	1 3	ax-mp	⊢ ( EndoFMnd ‘ ∅ ) ∈ Mnd