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 \in V, n \in V ⟼ n^{(m \times m)})$

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 \times m)$
8	4 7 5	co	$class (n^{(m \times m)})$
9	1 3 2 2 8	cmpo	$class (m \in V, n \in V ⟼ n^{(m \times m)})$
10	0 9	wceq	$wff intOp = (m \in V, n \in V ⟼ n^{(m \times m)})$