Metamath Proof Explorer


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 ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = { ∅ }

Proof

Step Hyp Ref Expression
1 eqid ( EndoFMnd ‘ ∅ ) = ( EndoFMnd ‘ ∅ )
2 eqid ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = ( Base ‘ ( EndoFMnd ‘ ∅ ) )
3 1 2 efmndbas ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = ( ∅ ↑m ∅ )
4 0map0sn0 ( ∅ ↑m ∅ ) = { ∅ }
5 3 4 eqtri ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = { ∅ }