Metamath Proof Explorer

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 ` (/) ) e. Mnd

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 eqid 
 |-  ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) )
3 2 efmndmnd 
 |-  ( (/) e. _V -> ( EndoFMnd ` (/) ) e. Mnd )
4 1 3 ax-mp 
 |-  ( EndoFMnd ` (/) ) e. Mnd