Description: Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-intop |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cintop | ||
1 | vm | ||
2 | cvv | ||
3 | vn | ||
4 | 3 | cv | |
5 | cmap | ||
6 | 1 | cv | |
7 | 6 6 | cxp | |
8 | 4 7 5 | co | |
9 | 1 3 2 2 8 | cmpo | |
10 | 0 9 | wceq |