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