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	$$⊢\mathrm{intOp}=\left(m\in \mathrm{V},n\in \mathrm{V}⟼n^{\left(m\times m\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cintop	$$class\mathrm{intOp}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4	3	cv	$$setvarn$$
5		cmap	$$class{\uparrow }_{𝑚}$$
6	1	cv	$$setvarm$$
7	6 6	cxp	$$class\left(m\times m\right)$$
8	4 7 5	co	$$class\left(n^{\left(m\times m\right)}\right)$$
9	1 3 2 2 8	cmpo	$$class\left(m\in \mathrm{V},n\in \mathrm{V}⟼n^{\left(m\times m\right)}\right)$$
10	0 9	wceq	$$wff\mathrm{intOp}=\left(m\in \mathrm{V},n\in \mathrm{V}⟼n^{\left(m\times m\right)}\right)$$