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 ` (/) ) ) = { (/) }