Metamath Proof Explorer


Definition df-intop

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 intOp = m V , n V n m × m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cintop class intOp
1 vm setvar m
2 cvv class V
3 vn setvar n
4 3 cv setvar n
5 cmap class 𝑚
6 1 cv setvar m
7 6 6 cxp class m × m
8 4 7 5 co class n m × m
9 1 3 2 2 8 cmpo class m V , n V n m × m
10 0 9 wceq wff intOp = m V , n V n m × m