This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⁡ ∅ = ∅ ∅
4 0map0sn0 ⊢ ∅ ∅ = ∅
5 3 4 eqtri ⊢ Base EndoFMnd ⁡ ∅ = ∅