Description: The monoid of endofunctions on a singleton has cardinality 1 . (Contributed by AV, 27-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | efmnd1bas.1 | No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |- | |
efmnd1bas.2 | |
||
efmnd1bas.0 | |
||
Assertion | efmnd1hash | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efmnd1bas.1 | Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |- | |
2 | efmnd1bas.2 | |
|
3 | efmnd1bas.0 | |
|
4 | snfi | |
|
5 | 3 4 | eqeltri | |
6 | 1 2 | efmndhash | |
7 | 5 6 | ax-mp | |
8 | 3 | fveq2i | |
9 | hashsng | |
|
10 | 8 9 | eqtrid | |
11 | 10 10 | oveq12d | |
12 | 1z | |
|
13 | 1exp | |
|
14 | 12 13 | ax-mp | |
15 | 11 14 | eqtrdi | |
16 | 7 15 | eqtrid | |