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 ⁡ ∅ ∈ 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